English
For a unit x in CliffordAlgebra Q, the image under the coe map lies in LipschitzGroup if and only if x is in LipschitzGroup and its image lies in unitary.
Русский
Для единицы x в CliffordAlgebra Q образ через coe принадлежит LipschitzGroup тогда и только тогда, когда сама единица принадлежит LipschitzGroup и её образ лежит в unitary.
LaTeX
$$$$\\uparrow x \\in (\\mathrm{lipschitzGroup}(Q)) \\\\_toSubmonoid.map \\mathrm{Units.coeHom} (\\mathrm CliffordAlgebra Q) \\iff x \\in \\mathrm{lipschitzGroup}(Q).$$$$
Lean4
theorem coe_mem_iff_mem {x : (CliffordAlgebra Q)ˣ} :
↑x ∈ (lipschitzGroup Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) ↔ x ∈ lipschitzGroup Q :=
by
simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]
norm_cast
exact exists_eq_right
