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, 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

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

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