Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces
|
1 |
a * 0 = 0 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) example : a * 0 = 0 := sorry |
Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que
|
1 |
a + b = c + b |
entonces
|
1 |
a = c |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} example (h : a + b = c + b) : a = c := sorry |
Read More «Si R es un anillo y a, b, c ∈ R tales que a+b=c+b, entonces a=c»
Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que
|
1 |
a + b = a + c |
entonces
|
1 |
b = c |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} example (h : a + b = a + c) : b = c := sorry |
Read More «Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c»