{"id":1261,"date":"2023-07-13T06:00:58","date_gmt":"2023-07-13T04:00:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1261"},"modified":"2023-07-19T12:35:09","modified_gmt":"2023-07-19T10:35:09","slug":"13-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/13-jul-23\/","title":{"rendered":"\u2200 a b c \u2208 \u211d, a(bc) = b(ac)"},"content":{"rendered":"

Demostrar con Lean4 que \u2200 a b c \u2208 \u211d, a * (b * c) = b * (a * c)<\/p>\n

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

\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Real.Basic\r\n\r\nexample\r\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\r\nby sorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nPor la siguiente cadena de igualdades:
\n\\begin{align}
\n   a(bc)
\n   &= (ab)c    &&\\text{[por la asociativa]} \\\\
\n   &= (ba)c    &&\\text{[por la conmutativa]} \\\\
\n   &= b(ac)    &&\\text{[por la asociativa]}
\n\\end{align}<\/p>\n
Demostraciones con Lean<\/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) : a * (b * c) = b * (a * c) :=\r\ncalc\r\n  a * (b * c)\r\n    = (a * b) * c := by rw [\u2190mul_assoc]\r\n  _ = (b * a) * c := by rw [mul_comm a b]\r\n  _ = b * (a * c) := by rw [mul_assoc]\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\r\nby\r\n  rw [\u2190mul_assoc]\r\n  rw [mul_comm a b]\r\n  rw [mul_assoc]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\r\nby ring\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