toUnits — Mathlib

English

There is a natural monoid homomorphism from pinGroup Q into the units of CliffordAlgebra Q, sending x to the unit with value x and inverse x^{-1}.

Русский

Существует естественное гомоморфное отображение от pinGroup Q в единицы CliffordAlgebra Q, отправляющее x в соответствующую единицу с значением x и обратное x^{-1}.

LaTeX

$$toUnits : pinGroup Q →* (CliffordAlgebra Q)ˣ$$

Lean4

/-- The elements in `pinGroup Q` embed into (CliffordAlgebra Q)ˣ. -/
@[simps]
def toUnits : pinGroup 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

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