Resta_igual_suma_opuesto.md

Título	Autor
Si R es un anillo y a, b ∈ R, entonces a - b = a + -b	José A. Alonso

[mathjax] 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

Demostración en lenguaje natural

Por la definición de la resta.

Demostraciones con Lean4

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a b : R)

example : a - b = a + -b :=
-- by exact?
sub_eq_add_neg a b

Demostraciones interactivas

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 12.