{"id":1414,"date":"2023-07-31T06:00:08","date_gmt":"2023-07-31T04:00:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1414"},"modified":"2023-07-23T18:36:14","modified_gmt":"2023-07-23T16:36:14","slug":"31-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/31-jul-23\/","title":{"rendered":"Si R es un anillo y a, b \u2208 R, entonces (a + b) + -b = a"},"content":{"rendered":"

En Lean4, se declara que R es un anillo mediante la expresi\u00f3n<\/p>\n

\r\n   variable {R : Type _} [Ring R]\r\n<\/pre>\n
Como consecuencia, se tiene los siguientes axiomas<\/p>\n
\r\n   add_assoc    : \u2200 a b c : R, (a + b) + c = a + (b + c)\r\n   add_comm     : \u2200 a b : R,   a + b = b + a\r\n   zero_add     : \u2200 a : R,     0 + a = a\r\n   add_left_neg : \u2200 a : R,     -a + a = 0\r\n   mul_assoc    : \u2200 a b c : R, a * b * c = a * (b * c)\r\n   mul_one      : \u2200 a : R,     a * 1 = a\r\n   one_mul      : \u2200 a : R,     1 * a = a\r\n   mul_add      : \u2200 a b c : R, a * (b + c) = a * b + a * c\r\n   add_mul      : \u2200 a b c : R, (a + b) * c = a * c + b * c\r\n<\/pre>\n
Demostrar que si R es un anillo, entonces<\/p>\n
\r\n   \u2200 a, b : R, (a + b) + -b = a\r\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable (a b : R)\r\n\r\nexample : (a + b) + -b = a :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nPor la siguiente cadena de igualdades
\n\\begin{align}
\n(a + b) + -b &= a + (b + -b)    &&\\text{[por la asociativa]} \\\\
\n             &= a + 0           &&\\text{[por suma con opuesto]} \\\\
\n             &= a               &&\\text{[por suma con cero]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\n\r\nvariable {R : Type _} [Ring R]\r\nvariable (a b : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\r\ncalc\r\n  (a + b) + -b = a + (b + -b) := by rw [add_assoc]\r\n             _ = a + 0        := by rw [add_right_neg]\r\n             _ = a            := by rw [add_zero]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\r\nby\r\n  rw [add_assoc]\r\n  rw [add_right_neg]\r\n  rw [add_zero]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\r\nby rw [add_assoc, add_right_neg, add_zero]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\r\n  add_neg_cancel_right a b\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\r\n  add_neg_cancel_right _ _\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample : (a + b) + -b = a :=\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