{"id":1427,"date":"2023-08-03T06:00:45","date_gmt":"2023-08-03T04:00:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1427"},"modified":"2023-07-27T12:18:49","modified_gmt":"2023-07-27T10:18:49","slug":"03-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/03-ago-23\/","title":{"rendered":"Si R es un anillo y a \u2208 R, entonces a.0 = 0"},"content":{"rendered":"

Demostrar con Lean4 que si R es un anillo y a \u2208 R, entonces<\/p>\n

\r\n   a * 0 = 0\r\n<\/pre>\n
Para 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 : a * 0 = 0 :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nBasta aplicar la propiedad cancelativa a
\n\\[a.0 + a.0 = a.0 + 0\\]
\nque se demuestra mediante la siguiente cadena de igualdades
\n\\begin{align}
\n   a.0 + a.0 &= a.(0 + 0)    &&\\text{[por la distributiva]} \\\\
\n             &= a.0          &&\\text{[por suma con cero]} \\\\
\n             &= a.0 + 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\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\nby\r\n  have h : a * 0 + a * 0 = a * 0 + 0 :=\r\n    calc a * 0 + a * 0 = a * (0 + 0) := by rw [mul_add a 0 0]\r\n                     _ = a * 0       := by rw [add_zero 0]\r\n                     _ = a * 0 + 0   := by rw [add_zero (a * 0)]\r\n  rw [add_left_cancel h]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\nby\r\n  have h : a * 0 + a * 0 = a * 0 + 0 :=\r\n    calc a * 0 + a * 0 = a * (0 + 0) := by rw [\u2190 mul_add]\r\n                     _ = a * 0       := by rw [add_zero]\r\n                     _ = a * 0 + 0   := by rw [add_zero]\r\n  rw [add_left_cancel h]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\nby\r\n  have h : a * 0 + a * 0 = a * 0 + 0 :=\r\n    by rw [\u2190 mul_add, add_zero, add_zero]\r\n  rw [add_left_cancel h]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\nby\r\n  have : a * 0 + a * 0 = a * 0 + 0 :=\r\n    calc a * 0 + a * 0 = a * (0 + 0) := by simp\r\n                     _ = a * 0       := by simp\r\n                     _ = a * 0 + 0   := by simp\r\n  simp\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\n  mul_zero a\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : a * 0 = 0 :=\r\nby simp\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n