Los monoides booleanos son conmutativos

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide \(M\) es booleano si
\[ (∀ x ∈ M)[x·x = 1] \]
y es conmutativo si
\[ (∀ x, y ∈ M)[x·y = y·x] \]

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

Demostrar con Lean4 que los monoides booleanos son conmutativos.

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

Read More «Los monoides booleanos son conmutativos»