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

Demostrar con Lean4 que los n\u00fameros reales tienen la siguiente propiedad<\/p>\n

\r\n(a * b) * c = b * (a * c)\r\n<\/pre>\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 (a b c : \u211d) : (a * b) * c = b * (a * c) := by\r\nsorry\r\n<\/pre>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

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