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
1 2 3 |
mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a |
Demostrar con Lean4 que los monoides booleanos son conmutativos.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by sorry |