Demostrar con Lean4 que los n\u00fameros reales tienen la siguiente propiedad<\/p>\n
\r\n(c * b) * a = b * (a * c)\r\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Real.Basic\r\n\r\nexample (a b c : \u211d) : (c * b) * a = b * (a * c) :=\r\nby sorry\r\n<\/pre>\nDemostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de igualdades:
\n\\begin{align}
\n (cb)a
\n &= (bc)a &&\\text{[por la conmutativa]} \\\\
\n &= b(ca) &&\\text{[por la asociativa]} \\\\
\n &= b(ac) &&\\text{[por la conmutativa]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Real.Basic\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (a b c : \u211d)\r\n : (c * b) * a = b * (a * c) :=\r\ncalc\r\n (c * b) * a\r\n = (b * c) * a := by rw [mul_comm c b]\r\n _ = b * (c * a) := by rw [mul_assoc]\r\n _ = b * (a * c) := by rw [mul_comm c a]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (a b c : \u211d)\r\n : (c * b) * a = b * (a * c) :=\r\nby\r\n rw [mul_comm c b]\r\n rw [mul_assoc]\r\n rw [mul_comm c a]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (a b c : \u211d)\r\n : (c * b) * a = b * (a * c) :=\r\nby ring\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