{"id":1438,"date":"2023-08-08T06:00:00","date_gmt":"2023-08-08T04:00:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1438"},"modified":"2023-07-28T18:45:22","modified_gmt":"2023-07-28T16:45:22","slug":"08-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/08-ago-23\/","title":{"rendered":"Si R es un anillo y a, b \u2208 R tales que a+b=0, entonces a=-b"},"content":{"rendered":"

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

\r\n   a + b = 0\r\n<\/pre>\n
entonces<\/p>\n
\r\n   a = -b\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 b : R}\r\n\r\nexample\r\n  (h : a + b = 0)\r\n  : a = -b :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\n   a &= (a + b) + -b    &&\\text{[por la concelativa]} \\\\
\n     &= 0 + -b          &&\\text{[por la hip\u00f3tesis]} \\\\
\n     &= -b              &&\\text{[por la suma con cero]}
\n\\end{align}<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Sumando \\(-a\\) a ambos lados de la hip\u00f3tesis, se tiene
\n\\[(a + b) + -b = 0 + -b\\]
\nEl t\u00e9rmino de la izquierda se reduce a \\(a\\) (por la cancelativa) y el de la derecha a \\(-b\\) (por la suma con cero). Por tanto, se tiene
\n\\[a = -b\\]<\/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 b : R}\r\n\r\n-- 1\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : a = -b :=\r\ncalc\r\n  a = (a + b) + -b := by rw [add_neg_cancel_right]\r\n  _ = 0 + -b       := by rw [h]\r\n  _ = -b           := by rw [zero_add]\r\n\r\n-- 2\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : a = -b :=\r\ncalc\r\n  a = (a + b) + -b := by simp\r\n  _ = 0 + -b       := by rw [h]\r\n  _ = -b           := by simp\r\n\r\n-- 3\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : a = -b :=\r\nby\r\n  have h1 : (a + b) + -b = 0 + -b := by rw [h]\r\n  have h2 : (a + b) + -b = a := add_neg_cancel_right a b\r\n  have h3 : 0 + -b = -b := zero_add (-b)\r\n  rwa [h2, h3] at h1\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = 0)\r\n  : a = -b :=\r\nadd_eq_zero_iff_eq_neg.mp h\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