Si a+b = c, entonces (a+b)(a+b) = ac+ bc
Demostrar con Lean4 que si a, b y c son números reales tales que
|
1 |
a + b = c, |
entonces
|
1 |
(a + b) * (a + b) = a * c + b * c |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c : ℝ) example (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a + b)(a + b)
&= (a + b)c &&\text{[por la hipótesis]} \\
&= ac + bc &&\text{[por la distributiva]}
\end{align}
Demostraciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c : ℝ) -- 1ª demostración example (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := calc (a + b) * (a + b) = (a + b) * c := by exact congrArg (HMul.hMul (a + b)) h _ = a * c + b * c := by rw [add_mul] -- 2ª demostración example (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by nth_rewrite 2 [h] rw [add_mul] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 9.
