toUnits — Mathlib

English

The elements of the circle embed into the units of the complex numbers via a canonical monoid homomorphism.

Русский

Элементы окружности встраиваются в группу модулей комплексных чисел через канонический моноид-гомоморфизм.

LaTeX

$$$$ \\text{toUnits}: Circle \\to^{*} \\mathrm{Units}(\\mathbb{C}) $$$$

Lean4

/-- The elements of the circle embed into the units. -/
def toUnits : Circle →* Units ℂ :=
  unitSphereToUnits
    ℂ
      -- written manually because `@[simps]` generated the wrong lemma

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