punitCoprod — Mathlib

English

There is a natural isomorphism between PUnit ∗ M and M, dual to the previous one, showing the symmetry with respect to the unit.

Русский

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

LaTeX

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

Lean4

/-- Isomorphism between `PUnit ∗ M` and `M`. -/
@[to_additive (attr := simps! -fullyApplied) /-- Isomorphism between `AddMonoid.Coprod PUnit M` and `M`. -/
    ]
def punitCoprod : PUnit ∗ M ≃* M :=
  MonoidHom.toMulEquiv snd inr (hom_ext (Subsingleton.elim _ _) rfl) snd_comp_inr

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