Caracterización de producto igual al primer factor
Un monoide cancelativo por la izquierda es un monoide \(M\) que cumple la propiedad cancelativa por la izquierda; es decir, para todo \(a, b ∈ M\)
\[ a·b = a·c ↔ b = c \]
En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es
|
1 |
mul_left_cancel : a * b = a * c → b = c |
Demostrar con Lean4 que si \(M\) es un monoide cancelativo por la izquierda y \(a, b ∈ M\), entonces
\[ a·b = a ↔ b = 1 \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} example : a * b = a ↔ b = 1 := by sorry |
Read More «Caracterización de producto igual al primer factor»