En los anillos, 1 + 1 = 2
Demostrar con Lean4 que En los anillos, \(1 + 1 = 2\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] example : 1 + 1 = (2 : R) := sorry |
Demostración en lenguaje natural
Por cálculo.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] -- Demostraciones con Lean4 -- ======================== -- 1ª demostración example : 1 + 1 = (2 : R) := by norm_num -- 2ª demostración example : 1 + 1 = (2 : R) := one_add_one_eq_two |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 12.
