Demostrar que si R es un anillo y a, b ∈ R, entonces
|
1 |
a - b = a + -b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} example : a - b = a + -b := sorry |
Read More «Si R es un anillo y a, b ∈ R, entonces a – b = a + -b»
Demostrar que si R es un anillo y a ∈ R, entonces
|
1 |
-(-a) = a. |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variable a : R example : -(-a) = a := sorry |
Demostrar que si R es un anillo, entonces
|
1 |
-0 = 0 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.ring variables {R : Type*} [ring R] example : (-0 : R) = 0 := sorry |
Demostrar que si R es un anillo y a, b ∈ R tales que
|
1 |
a + b = 0 |
entonces
|
1 |
a = -b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} example (h : a + b = 0) : a = -b := sorry |
Read More «Si R es un anillo y a,b∈R tales que a+b=0, entonces a=-b»
Demostrar que Si R es un anillo y a, b ∈ R tales que
|
1 |
a + b = 0 |
entonces
|
1 |
-a = b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} example (h : a + b = 0) : -a = b := sorry |
Read More «Si R es un anillo y a,b∈R tales que a+b=0, entonces -a=b»
Demostrar que si R es un anillo y a ∈ R, entonces
|
1 |
0 * a = 0. |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variable (a : R) example : 0 * a = 0 := sorry |
Demostrar que Si R es un anillo y a ∈ R, entonces
|
1 |
a * 0 = 0 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variable a : R example : a * 0 = 0 := sorry |
Demostrar 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 Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {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 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 Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {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.»
Demostrar que si R es un anillo, entonces
|
1 |
∀ a b : R, (a + b) + -b = a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R example : (a + b) + -b = a := sorry |
Read More «Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a»