freeMonoidCongr — Mathlib

English

Free monoids over isomorphic types are isomorphic: if e: α ≃ β, then FreeMonoid α ≃* FreeMonoid β.

Русский

Свободные моноиды над изоморфными типами изоморфны: если e: α ≃ β, то FreeMonoid α ≃* FreeMonoid β.

LaTeX

$$$ FreeMonoid\alpha \cong FreeMonoid\beta $ (MulIsom)$$

Lean4

/-- free monoids over isomorphic types are isomorphic -/
@[to_additive /-- if two types are isomorphic, the additive free monoids over those types are
    isomorphic -/
    ]
def freeMonoidCongr (e : α ≃ β) : FreeMonoid α ≃* FreeMonoid β
    where
  toFun := FreeMonoid.map ⇑e
  invFun := FreeMonoid.map ⇑e.symm
  left_inv _ := map_symm_apply_map_eq e
  right_inv _ := map_apply_map_symm_eq e
  map_mul' := by simp [map_mul]

Похожие утверждения