{"id":1454,"date":"2023-08-14T06:09:09","date_gmt":"2023-08-14T04:09:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1454"},"modified":"2023-07-30T17:51:56","modified_gmt":"2023-07-30T15:51:56","slug":"14-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/14-ago-23\/","title":{"rendered":"Si R es un anillo y a \u2208 R, entonces a – a = 0"},"content":{"rendered":"


\nDemostrar con Lean4 que si \\(R\\) es un anillo y \\(a \\in R\\), entonces
\n\\[a – a = 0\\]<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\r\nimport Mathlib.Algebra.Ring.Defs\r\nvariable {R : Type _} [Ring R]\r\nvariable (a : R)\r\n\r\nexample : a - a = 0 :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Por la siguiente cadena de igualdades:
\n\\begin{align}
\n   a – a &= a + -a    &&\\text{[por definici\u00f3n de resta]} \\\\
\n         &= 0         &&\\text{[por suma con opuesto]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Algebra.Ring.Defs\r\nvariable {R : Type _} [Ring R]\r\nvariable (a : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : a - a = 0 :=\r\ncalc\r\n  a - a = a + -a := by rw [sub_eq_add_neg a a]\r\n      _ = 0      := by rw [add_right_neg]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : a - a = 0 :=\r\nsub_self a\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : a - a = 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