English
If f : A →⋆* B is bijective as a function, then f induces a StarMulEquiv A B, i.e., a star-monoid isomorphism between A and B.
Русский
Если f : A →⋆* B относится к биективному отображению как к функции, то f индуцирует StarMulEquiv A B, то есть звёздное моноидное изоморфное соответствие между A и B.
LaTeX
$$$\\exists e : A ≃⋆* B\\, (\\mathrm{toFun}(e) = f)$$$
Lean4
/-- If a star monoid morphism has an inverse, it is an isomorphism of star monoids. -/
@[simps]
def ofStarMonoidHom (f : A →⋆* B) (g : B →⋆* A) (h₁ : g.comp f = .id _) (h₂ : f.comp g = .id _) : A ≃⋆* B
where
toFun := f
invFun := g
left_inv := DFunLike.ext_iff.mp h₁
right_inv := DFunLike.ext_iff.mp h₂
map_mul' := map_mul f
map_star' := map_star f
