English
The Lipschitz group Q is defined as the subgroup closure of all invertible elements of the form ι Q m, where ι is the canonical linear map M → CliffordAlgebra Q.
Русский
Группа Lipschitz(Q) определяется как замыкание по подгруппе всех обращимых элементов вида ι Q m, где ι — каноническое линейное отображение M → CliffordAlgebra Q.
LaTeX
$$$$\\mathrm{lipschitzGroup}(Q) = \\mathrm{Subgroup}.closure\\Big( (\\uparrow)^{-1} \\' \\mathrm{Im}(\\iota_Q) : \\{ ι_Q m : m \\in M \\} \\Big) $$$$
Lean4
/-- `lipschitzGroup` is the subgroup closure of all the invertible elements in the form of `ι Q m`
where `ι` is the canonical linear map `M →ₗ[R] CliffordAlgebra Q`. -/
def lipschitzGroup (Q : QuadraticForm R M) : Subgroup (CliffordAlgebra Q)ˣ :=
Subgroup.closure ((↑) ⁻¹' Set.range (ι Q) : Set (CliffordAlgebra Q)ˣ)
