mem_lipschitzGroup — Mathlib

English

If x is in pinGroup, then x is in the image of LipschitzGroup under the coe map.

Русский

Если x ∈ pinGroup, то x лежит в образе LipschitzGroup под отображением coe.

LaTeX

$$$$x \\in \\mathrm{pinGroup}(Q) \\Rightarrow x \\in (\\mathrm{lipschitzGroup}(Q)).toSubmonoid.map (\\mathrm{Units.coeHom} \\lvert\\!\\!\\mathrm CliffordAlgebra Q).$$$$

Lean4

theorem mem_lipschitzGroup {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) :
    x ∈ (lipschitzGroup Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) :=
  hx.1

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