Demostrar con Lean4 que si R es un anillo y a \u2208 R, entonces<\/p>\n
\r\n -(-a) = a\r\n<\/pre>\nPara 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) = a :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nEs consecuencia de las siguiente propiedades demostradas en ejercicios anteriores:
\n\\begin{align}
\n &\\forall a \\ b \\in R, a + b = 0 \\to -a = b \\\\
\n &\\forall a \\in R, -a + a = 0
\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\nexample : -(-a) = a :=\r\nby\r\n have h1 : -a + a = 0 := add_left_neg a\r\n show -(-a) = a\r\n exact neg_eq_of_add_eq_zero_right h1\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : -(-a) = a :=\r\nby\r\n apply neg_eq_of_add_eq_zero_right\r\n rw [add_left_neg]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : -(-a) = a :=\r\nneg_neg a\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : -(-a) = a :=\r\nby simp\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n