toUnits — Mathlib

English

The mapping toUnits preserves the unit structure and maps the identity to the identity.

Русский

Любое отображение toUnits сохраняет единичную структуру и отображает единицу в единицу.

LaTeX

$$toUnits(1) = 1 in (CliffordAlgebra(Q))^{\times}.$$

Lean4

/-- The elements in `spinGroup Q` embed into (CliffordAlgebra Q)ˣ. -/
@[simps]
def toUnits : spinGroup Q →* (CliffordAlgebra Q)ˣ
    where
  toFun x := ⟨x, ↑x⁻¹, coe_mul_star_self x, coe_star_mul_self x⟩
  map_one' := Units.ext rfl
  map_mul' _x _y := Units.ext rfl

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