En los monoides, los inversos a la izquierda y a la derecha son iguales
Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.
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 que si \(M\) es un monoide, \(a ∈ M\), \(b\) es un inverso de \(a\) por la izquierda y \(c\) es un inverso de \(a\) por la derecha, entonces \(b = c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Group.Defs variable {M : Type} [Monoid M] variable {a b c : M} example (hba : b * a = 1) (hac : a * c = 1) : b = c := by sorry |
Read More «En los monoides, los inversos a la izquierda y a la derecha son iguales»