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 |