English
Two auxiliary changes interact: applying changeFormAuxChangeFormAux twice yields (Q v − B v v) times the second argument, i.e., a quadratic correction term appears when chaining two applications.
Русский
Две вспомогательные константы взаимодействуют: применение changeFormAux_changeFormAux дважды эквивалентно умножению на скаляр (Qv − Bv v) при втором аргументе, т.е. появляется квадратичный поправочный член при последовательном применении.
LaTeX
$$$\\text{changeFormAux\_changeFormAux}(Q, B, v, x) = (Q(v) - B(v,v)) \\cdot x.$$$
Lean4
theorem changeFormAux_changeFormAux (B : BilinForm R M) (v : M) (x : CliffordAlgebra Q) :
changeFormAux Q B v (changeFormAux Q B v x) = (Q v - B v v) • x :=
by
simp only [changeFormAux_apply_apply]
rw [mul_sub, ← mul_assoc, ι_sq_scalar, map_sub, contractLeft_ι_mul, ← sub_add, sub_sub_sub_comm, ← Algebra.smul_def,
sub_self, sub_zero, contractLeft_contractLeft, add_zero, sub_smul]
