Skip to main content

Si R es un anillo y a ∈ R, entonces -(-a) = a

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

Demostración en lenguaje natural

Es consecuencia de las siguiente propiedades demostradas en ejercicios anteriores: \begin{align} &\forall a \ b \in R, a + b = 0 \to -a = b \\ &\forall a \in R, -a + a = 0 \end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic

variable {R : Type _} [Ring R]
variable {a : R}

-- 1ª demostración
example : -(-a) = a :=
by
  have h1 : -a + a = 0 := neg_add_cancel a
  show -(-a) = a
  exact neg_eq_of_add_eq_zero_right h1

-- 2ª demostración
example : -(-a) = a :=
by
  apply neg_eq_of_add_eq_zero_right
  rw [neg_add_cancel]

-- 3ª demostración
example : -(-a) = a :=
neg_neg a

-- 4ª demostración
example : -(-a) = a :=
by simp

-- Lemas usados
-- ============

-- variable (b : R)
-- #check (neg_add_cancel a : -a + a = 0)
-- #check (neg_eq_of_add_eq_zero_right : a + b = 0 → -a = b)
-- #check (neg_neg a : -(-a) = a)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias