--- Título: Si R es un anillo y a ∈ R, entonces -(-a) = a Autor: José A. Alonso --- 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 [mathjax] 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 := add_left_neg 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 [add_left_neg]

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

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

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

J. Avigad y P. Massot. Mathematics in Lean, p. 11.