Demostrar con Lean4 que si \(G\) es un grupo y \(a \in G\), entonces
\[a·1 = a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * 1 = a := sorry |
En Lean4, se declara que \(G\) es un grupo mediante la expresión
|
1 |
variable {G : Type _} [Group G] |
Como consecuencia, se tiene los siguientes axiomas
|
1 2 3 |
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) one_mul : ∀ a : G, 1 * a = a mul_left_inv : ∀ a : G, a⁻¹ * a = 1 |
Demostrar que si \(G\) es un grupo y \(a \in G\), entonces
\[aa⁻¹ = 1\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * a⁻¹ = 1 := sorry |
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces
\[2a = a+a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a : R) example : 2 * a = a + a := sorry |
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 |
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces
\[a – a = 0\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a : R) example : a - a = 0 := sorry |
Demostrar con Lean4 que si \(R\) es un anillo y \(a, b \in R\), entonces
\[a – b = a + -b\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (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 con Lean4 que si R es un anillo y a ∈ R, entonces
|
1 |
-(-a) = a |
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) = a := sorry |
Demostrar con Lean4 que si R es un anillo, entonces
|
1 |
-0 = 0 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] example : (-0 : R) = 0 := sorry |
Demostrar con Lean4 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 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 : 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 con Lean4 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 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 : 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»