English
The quotient map from the free monoid to the presented monoid with relations rels is a monoid hom.
Русский
Квазиобразующее отображение из свободного моноида в presentedMonoid rels является гомоморфизмом моноидов.
LaTeX
$$$\\mathrm{mk}: \\mathrm{FreeMonoid}(\\alpha) \\to^* \\mathrm{PresentedMonoid}(rels)$ is a monoid hom$$
Lean4
/-- The quotient map from the free monoid on `α` to the presented monoid with the same generators
and the given relations `rels`. -/
@[to_additive /-- The quotient map from the free additive monoid on `α` to the presented additive
monoid with the same generators and the given relations `rels` -/
]
def mk (rels : FreeMonoid α → FreeMonoid α → Prop) : FreeMonoid α →* PresentedMonoid rels
where
toFun := Quotient.mk (conGen rels).toSetoid
map_one' := rfl
map_mul' := fun _ _ => rfl
