Si a, b y c son números reales, entonces (a * b) * c = b * (a * c)
Demostrar que los números reales tienen la siguiente propiedad
|
1 |
(a * b) * c = b * (a * c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic variables a b c : ℝ example : (a * b) * c = b * (a * c) := 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 |
import data.real.basic variables a b c : ℝ -- 1ª demostración -- =============== example : (a * b) * c = b * (a * c) := begin rw mul_comm a b, rw mul_assoc b a c, end -- 2ª demostración -- =============== example : (a * b) * c = b * (a * c) := calc (a * b) * c = (b * a) * c : by rw mul_comm a b ... = b * (a * c) : by rw mul_assoc b a c -- 3ª demostración -- =============== example : (a * b) * c = b * (a * c) := calc (a * b) * c = (b * a) * c : by ring ... = b * (a * c) : by ring -- 4ª demostración -- =============== example : (a * b) * c = b * (a * c) := by ring |
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. 5.
