Si a, b, c y d son números reales, entonces (a + b) * (c + d) = a * c + a * d + b * c + b * d
Demostrar que si a, b, c y d son números reales, entonces
|
1 |
(a + b) * (c + d) = a * c + a * d + b * c + b * d |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.real.basic variables a b c d : ℝ example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
import data.real.basic variables a b c d : ℝ -- 1ª demostración -- =============== example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) : by rw add_mul ... = a * c + a * d + b * (c + d) : by rw mul_add ... = a * c + a * d + (b * c + b * d) : by rw mul_add ... = a * c + a * d + b * c + b * d : by rw ←add_assoc -- 2ª demostración -- =============== example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) : by ring ... = a * c + a * d + b * (c + d) : by ring ... = a * c + a * d + (b * c + b * d) : by ring ... = a * c + a * d + b * c + b * d : by ring -- 3ª demostración -- =============== example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by ring -- 4ª demostración -- =============== example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := begin rw add_mul, rw mul_add, rw mul_add, rw ← add_assoc, end -- 5ª demostración -- =============== example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by rw [add_mul, mul_add, mul_add, ←add_assoc] |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 8.
