Producto_por_dos.md

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

Demostrar con Lean4 que si (R) es un anillo y (a \in R), entonces [2a = a+a]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Ring.Defs

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

example : 2 * a = a + a :=
sorry

Demostración en lenguaje natural

[mathjax] Por la siguiente cadena de igualdades \begin{align} 2·a &= (1 + 1)·a &&\text{[por la definición de 2]} \ &= 1·a + 1·a &&\text{[por la distributiva]} \ &= a + a &&\text{[por producto con uno]} \end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Ring.Defs

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

-- 1ª demostración
example : 2 * a = a + a :=
calc
  2 * a = (1 + 1) * a   := by rw [one_add_one_eq_two]
      _ = 1 * a + 1 * a := by rw [add_mul]
      _ = a + a         := by rw [one_mul]

-- 2ª demostración
example : 2 * a = a + a :=
by exact two_mul a

Demostraciones interactivas

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

Referencias

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