{"id":1432,"date":"2023-08-07T06:00:51","date_gmt":"2023-08-07T04:00:51","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1432"},"modified":"2023-07-28T14:00:53","modified_gmt":"2023-07-28T12:00:53","slug":"07-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/07-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
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n

\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de igualdades
\n\\begin{align}
\n   -a &= -a + 0          &&\\text{[por suma cero]} \\\\
\n      &= -a + (a + b)    &&\\text{[por hip\u00f3tesis]} \\\\
\n      &= b               &&\\text{[por cancelativa]}
\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 + (a + b) = -a + 0\\]
\nEl t\u00e9rmino de la izquierda se reduce a \\(b\\) (por la cancelativa) y el de la derecha a \\(-a\\) (por la suma con cero). Por tanto, se tiene
\n\\[b = -a\\]
\nPor la simetr\u00eda de la igualdad, 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\u00ba en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : -a = b :=\r\ncalc\r\n  -a = -a + 0       := by rw [add_zero]\r\n   _ = -a + (a + b) := by rw [h]\r\n   _ = b            := by rw [neg_add_cancel_left]\r\n\r\n-- 2\u00aa demostraci\u00f3n (basada en la 1\u00ba en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : -a = b :=\r\ncalc\r\n  -a = -a + 0       := by simp\r\n   _ = -a + (a + b) := by rw [h]\r\n   _ = b            := by simp\r\n\r\n-- 3\u00aa demostraci\u00f3n (basada en la 2\u00ba en LN)\r\nexample\r\n  (h : a + b = 0)\r\n  : -a = b :=\r\nby\r\n  have h1 : -a + (a + b) = -a + 0 := congrArg (HAdd.hAdd (-a)) h\r\n  have h2 : -a + (a + b) = b := neg_add_cancel_left a b\r\n  have h3 : -a + 0 = -a := add_zero (-a)\r\n  rw [h2, h3] at h1\r\n  exact h1.symm\r\n\r\n-- 4\u00aa demostraci\u00f3n (con la librer\u00eda mathlib)\r\nexample\r\n  (h : a + b = 0)\r\n  : -a = b :=\r\nneg_eq_iff_add_eq_zero.mpr 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