Si R es un anillo y a ∈ R, entonces 2a = a+a

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]

variable (a : R)

example : 2 * a = a + a :=

sorry

Demostración en lenguaje natural

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

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.

Share this:

Escribe un comentarioCancel reply