Demostrar con Lean4 que si R es un anillo, entonces<\/p>\n
\r\n -0 = 0\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\n\r\nexample : (-0 : R) = 0 :=\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 suma con cero se tiene
\n\\[0 + 0 = 0\\]
\nAplic\u00e1ndole la propiedad
\n\\[\\forall a b \u2208 R, a + b = 0 \\to -a = b\\]
\nse obtiene
\n\\[-0 = 0\\]<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Puesto que
\n\\[\\forall a b \u2208 R, a + b = 0 \\to -a = b\\]
\nbasta demostrar que
\n\\[0 + 0 = 0\\]
\nque es cierta por la suma con cero.<\/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\n\r\n-- 1\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample : (-0 : R) = 0 :=\r\nby\r\n have h1 : (0 : R) + 0 = 0 := add_zero 0\r\n show (-0 : R) = 0\r\n exact neg_eq_of_add_eq_zero_left h1\r\n\r\n-- 2\u00aa demostraci\u00f3n (basada en la 2\u00aa en LN)\r\nexample : (-0 : R) = 0 :=\r\nby\r\n apply neg_eq_of_add_eq_zero_left\r\n rw [add_zero]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : (-0 : R) = 0 :=\r\n neg_zero\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : (-0 : R) = 0 :=\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