Demostrar con Lean4 que En los anillos, \(1 + 1 = 2\)
Para ello, completar la siguiente teoría de Lean4:
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:
import Mathlib.Algebra.Ring.Defs import Mathlib.Algebra.Group.Basic 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:
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a b : R) example : a - b = a + -b := sorry
Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces \[ -(-a) = a \]
Para ello, completar la siguiente teoría de Lean4:
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 \[ -0 = 0 \]
Para ello, completar la siguiente teoría de Lean4:
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 \[ a + b = 0 \] entonces \[ a = -b \]
Para ello, completar la siguiente teoría de Lean4:
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
Demostrar con Lean4 que si R es un anillo y a, b ∈ R tales que \[ a + b = 0 \] entonces \[ -a = b \]
Para ello, completar la siguiente teoría de Lean4:
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
Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces \[ 0·a = 0 \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable (a : R) example : 0 * a = 0 := sorry
Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces \[ a·0 = 0 \]
Para ello, completar la siguiente teoría de Lean4:
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 \[ a + b = c + b \] entonces \[ a = c \]
Para ello, completar la siguiente teoría de Lean4:
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