English
Define an auxiliary linear map that, for each v ∈ M, assigns the endomorphism of the Clifford algebra given by left multiplication by ι_Q(v) minus the contraction by the bilinear form B evaluated at v.
Русский
Определено вспомогательное линейное отображение, такое что для каждого v ∈ M отображает эндоморфизм CliffordAlgebra: левое умножение на ι_Q(v) минус согласованная конракция по B(v).
LaTeX
$$$\\text{changeFormAux}(B) : M \\to\\!_R (\\mathrm{CliffordAlgebra}(Q) \\to\\!_R \\mathrm{CliffordAlgebra}(Q)) \\,;\\; (\\text{changeFormAux}(B))(v) = L_{\\iota_Q(v)} - \\text{contractLeft}(B(v)).$$$
Lean4
/-- Auxiliary construction for `CliffordAlgebra.changeForm` -/
@[simps!]
def changeFormAux (B : BilinForm R M) : M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q :=
haveI v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
v_mul - contractLeft ∘ₗ B
