expEquiv — Mathlib

English

Let G be a group under addition. There exists a natural isomorphism expEquiv between the additive group G and the unit group of the zero-with-multiplicative construction of G, given by the exponential map.

Русский

Пусть G—группа по сложению. Существуют естественное изоморфизм expEquiv между аддитивной группой G и группой единиц WithZero(Multiplicative G), задаваемый экспонентой.

LaTeX

$$$\expEquiv: G \cong (G^{\mathrm{m0}})^{\times}$$$

Lean4

/-- The exponential map as an equivalence between `G` and `(Gᵐ⁰)ˣ`. -/
def expEquiv : G ≃ (Gᵐ⁰)ˣ :=
  Multiplicative.ofAdd.trans unitsWithZeroEquiv.symm.toEquiv

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