logEquiv — Mathlib

English

There is a natural isomorphism logEquiv between the unit group (Gᵐ⁰)ˣ and the additive group G, given by the logarithm map.

Русский

Существует натуральный изоморфизм logEquiv между группой единиц (Gᵐ⁰)ˣ и аддитивной группой G, задаваемый логарифмом.

LaTeX

$$$\logEquiv: (G^{\mathrm{m0}})^{\times} \simeq G$$$

Lean4

/-- The logarithm as an equivalence between `(Gᵐ⁰)ˣ` and `G`. -/
def logEquiv : (Gᵐ⁰)ˣ ≃ G :=
  unitsWithZeroEquiv.toEquiv.trans Multiplicative.toAdd

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