DAO: La semana en Calculemus (2 de septiembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

A continuación se muestran las soluciones.

1. Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b

En Lean, se declara que R es un anillo mediante la expresión

y, como consecuencia, se tienen los siguientes axiomas

Demostrar que si R es un anillo, entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

2. Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a

Demostrar que si R es un anillo, entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

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

Demostrar que si R es un anillo y a, b, c ∈ R tales que

entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

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

Demostrar que si R es un anillo y a, b, c ∈ R tales que

entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

5. Si R es un anillo y a ∈ R, entonces a * 0 = 0

Demostrar que Si R es un anillo y a ∈ R, entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.