unitSphereToUnits — Mathlib

English

There is a monoid homomorphism from the unit sphere to the group of units of 𝕜, sending each sphere element to its corresponding unit.

Русский

Существет гомоморфизм моноидов от единичной сферы к группе единиц 𝕜, отображающий элемент сферы в соответствующий элемент-единицу.

LaTeX

$$$\text{unitSphereToUnits} : (S) \to^* (Units 𝕜)$$$

Lean4

/-- Monoid homomorphism from the unit sphere in a normed division ring to the group of units. -/
def unitSphereToUnits (𝕜 : Type*) [NormedDivisionRing 𝕜] : sphere (0 : 𝕜) 1 →* Units 𝕜 :=
  Units.liftRight (Submonoid.unitSphere 𝕜).subtype (fun x => Units.mk0 x <| ne_zero_of_mem_unit_sphere _) fun _x => rfl

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