English
From a bijective star-monoid homomorphism f: A →⋆* B, construct a StarMulEquiv A B; this requires the existence of an inverse map that preserves star and multiplication.
Русский
Из биективного звёздного моноидного гомоморфизма f: A →⋆* B строится StarMulEquiv A B; требуется существование обратной карты, сохраняющей звезду и умножение.
LaTeX
$$$\\text{There exists } e : A \\simeq⋆* B \\text{ with } e.toFun = f \\text{ and } e.map\\_star' = \\text{map\\_star } f$$$
Lean4
/-- Promote a bijective star monoid homomorphism to a star monoid equivalence. -/
noncomputable def ofBijective (f : A →⋆* B) (hf : Function.Bijective f) : A ≃⋆* B :=
{
MulEquiv.ofBijective f (hf : Function.Bijective
(f : A → B)) with
toFun := f
map_star' := map_star f }
