Demostrar con Lean4 que si \\(R\\) es un anillo y \\(a \\in R\\), entonces
\n\\[2a = a+a\\]<\/p>\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 : R)\r\n\r\nexample : 2 * a = a + 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 2\u00b7a &= (1 + 1)\u00b7a &&\\text{[por la definici\u00f3n de 2]} \\\\
\n &= 1\u00b7a + 1\u00b7a &&\\text{[por la distributiva]} \\\\
\n &= a + a &&\\text{[por producto con uno]}
\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 : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : 2 * a = a + a :=\r\ncalc\r\n 2 * a = (1 + 1) * a := by rw [one_add_one_eq_two]\r\n _ = 1 * a + 1 * a := by rw [add_mul]\r\n _ = a + a := by rw [one_mul]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : 2 * a = a + a :=\r\nby exact two_mul a\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