toAdditiveLeft — Mathlib

English

There is a canonical equivalence between Additive G ≃+o Additive H and Multiplicative G ≃*o H.

Русский

Существует каноническое эквивалентное соответствие между Additive G ≃+o Additive H и Multiplicative G ≃*o H.

LaTeX

$$$ \mathrm{toMultiplicativeLeft}: (\mathrm{Additive}\,G \simeq_o \mathrm{Additive}\,H) \to (\mathrm{Multiplicative}\,G \simeq_o^{*} H) $$$

Lean4

/-- Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`. -/
abbrev toAdditiveLeft {G H : Type*} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
    (G ≃*o Multiplicative H) ≃ (Additive G ≃+o H) :=
  OrderAddMonoidIso.toMultiplicativeRight.symm

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