toMultiplicativeRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Reinterpret `Additive G ≃+o H` as `G ≃*o Multiplicative H`. -/
def toMultiplicativeRight {G H : Type*} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
    (Additive G ≃+o H) ≃ (G ≃*o Multiplicative H)
    where
  toFun e := ⟨e.toAddEquiv.toMultiplicativeRight, by simp⟩
  invFun e := ⟨e.toMulEquiv.toAdditiveLeft, by simp⟩
  left_inv e := by ext; simp
  right_inv e := by ext; simp

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