toMultiplicativeLeft — Mathlib

English

A technical step ensuring the compatibility of additive and multiplicative structures in the left-direction equivalence.

Русский

Технический шаг, гарантирующий совместимость аддитивной и умножительной структур в левом направлении эквивалентности.

LaTeX

$$$ \text{proof}_1 = \text{(compatibility of structures)} $$$

Lean4

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

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