coprodPUnit — Mathlib

English

There is a natural isomorphism between M ∗ PUnit and M, showing that adjoining a unit does not change the coproduct up to isomorphism.

Русский

Существует естественный изоморфизм между M ∗ PUnit и M, что добавление единицы в копродукт не меняет копродуктовую структуру до изоморфизма.

LaTeX

$$$ M \\ast PUnit \\cong M. $$$

Lean4

/-- Isomorphism between `M ∗ PUnit` and `M`. -/
@[to_additive (attr := simps! -fullyApplied) /-- Isomorphism between `AddMonoid.Coprod M PUnit` and `M`. -/
    ]
def coprodPUnit : M ∗ PUnit ≃* M :=
  MonoidHom.toMulEquiv fst inl (hom_ext rfl <| Subsingleton.elim _ _) fst_comp_inl

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