instUniqueOrderAddMonoidIso — Mathlib

English

There is an equivalence between OrderMonoidIso G (Multiplicative H) and OrderAddMonoidIso (Additive G) H.

Русский

Существует эквивалентность между OrderMonoidIso G (Multiplicative H) и OrderAddMonoidIso (Additive G) H.

LaTeX

$$$ \mathrm{toAdditiveLeft}: \text{OrderMonoidIso } G (\mathrm{Multiplicative } H) \to \text{OrderAddMonoidIso } (\mathrm{Additive } G) H $$$

Lean4

instance instUniqueOrderAddMonoidIso {G H : Type*} [CommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H]
    [Unique (G ≃*o H)] : Unique (Additive G ≃+o Additive H) :=
  OrderMonoidIso.toAdditive.symm.unique

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