Skip to main content

Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c

Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que \[ a + b = a + c \] entonces \[ b = 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 = a + c)
  : b = c :=
sorry

Demostración en lenguaje natural (LN)

1ª demostración en LN

Por la siguiente cadena de igualdades \begin{align} b &= 0 + b &&\text{[por suma con cero]} \\ &= (-a + a) + b &&\text{[por suma con opuesto]} \\ &= -a + (a + b) &&\text{[por asociativa]} \\ &= -a + (a + c) &&\text{[por hipótesis]} \\ &= (-a + a) + c &&\text{[por asociativa]} \\ &= 0 + c &&\text{[por suma con opuesto]} \\ &= c &&\text{[por suma con cero]} \end{align}

2ª demostración en LN

Por la siguiente cadena de implicaciones \begin{align} a + b = a + c &\Longrightarrow -a + (a + b) = -a + (a + c) &&\text{[sumando -a]} \\ &\Longrightarrow (-a + a) + b = (-a + a) + c &&\text{[por la asociativa]} \\ &\Longrightarrow 0 + b = 0 + b &&\text{[suma con opuesto]} \\ &\Longrightarrow b = c &&\text{[suma con cero]} \end{align}

3ª demostración en LN

Por la siguiente cadena de igualdades \begin{align} b &= -a + (a + b) \\ &= -a + (a + c) &&\text{[por la hipótesis]} \\ &= c \end{align}

Demostraciones con Lean4

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

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

-- 1ª demostración
example
  (h : a + b = a + c)
  : b = c :=
calc
  b = 0 + b        := by rw [zero_add]
  _ = (-a + a) + b := by rw [neg_add_cancel]
  _ = -a + (a + b) := by rw [add_assoc]
  _ = -a + (a + c) := by rw [h]
  _ = (-a + a) + c := by rw [←add_assoc]
  _ = 0 + c        := by rw [neg_add_cancel]
  _ = c            := by rw [zero_add]

-- 2ª demostración
example
  (h : a + b = a + c)
  : b = c :=
by
  have h1 : -a + (a + b) = -a + (a + c) :=
    congrArg (HAdd.hAdd (-a)) h
  clear h
  rw [← add_assoc] at h1
  rw [neg_add_cancel] at h1
  rw [zero_add] at h1
  rw [← add_assoc] at h1
  rw [neg_add_cancel] at h1
  rw [zero_add] at h1
  exact h1

-- 3ª demostración
example
  (h : a + b = a + c)
  : b = c :=
calc
  b = -a + (a + b) := by rw [neg_add_cancel_left a b]
  _ = -a + (a + c) := by rw [h]
  _ = c            := by rw [neg_add_cancel_left]

-- 4ª demostración
example
  (h : a + b = a + c)
  : b = c :=
by
  rw [← neg_add_cancel_left a b]
  rw [h]
  rw [neg_add_cancel_left]

-- 5ª demostración
example
  (h : a + b = a + c)
  : b = c :=
by
  rw [← neg_add_cancel_left a b, h, neg_add_cancel_left]

-- 6ª demostración
example
  (h : a + b = a + c)
  : b = c :=
add_left_cancel h

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

-- #check (add_assoc a b c : (a + b) + c = a + (b + c))
-- #check (add_left_cancel : a + b = a + c → b = c)
-- #check (neg_add_cancel a : -a + a = 0)
-- #check (neg_add_cancel_left a b : -a + (a + b) = b)
-- #check (zero_add a :  0 + a = a)

Demostraciones interactivas

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

Referencias