Demostrar con Lean4 que si R es un anillo y a \u2208 R, entonces<\/p>\n
\r\n 0 * a = 0\r\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\nimport Mathlib.Tactic\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable (a : R)\r\n\r\nexample : 0 * a = 0 :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nBasta aplicar la propiedad cancelativa a
\n\\[0.a + 0.a = 0.a + 0\\]
\nque se demuestra mediante la siguiente cadena de igualdades
\n\\begin{align}
\n 0.a + 0.a &= (0 + 0).a &&\\text{[por la distributiva]} \\\\
\n &= 0.a &&\\text{[por suma con cero]} \\\\
\n &= 0.a + 0 &&\\text{[por suma con cero]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Algebra.Ring.Defs\r\nimport Mathlib.Tactic\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable (a : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nby\r\n have h : 0 * a + 0 * a = 0 * a + 0 :=\r\n calc 0 * a + 0 * a = (0 + 0) * a := by rw [add_mul]\r\n _ = 0 * a := by rw [add_zero]\r\n _ = 0 * a + 0 := by rw [add_zero]\r\n rw [add_left_cancel h]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nby\r\n have h : 0 * a + 0 * a = 0 * a + 0 :=\r\n by rw [\u2190add_mul, add_zero, add_zero]\r\n rw [add_left_cancel h]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nby\r\n have : 0 * a + 0 * a = 0 * a + 0 :=\r\n calc 0 * a + 0 * a = (0 + 0) * a := by simp\r\n _ = 0 * a := by simp\r\n _ = 0 * a + 0 := by simp\r\n simp\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nby\r\n have : 0 * a + 0 * a = 0 * a + 0 := by simp\r\n simp\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nby simp\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample : 0 * a = 0 :=\r\nzero_mul a\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n