English
The map δAux is a derivation: δAux(xy) = x · δAux(y) + y · δAux(x) for generators x,y in the cotangent ring Q.Ring.
Русский
δAux является деривацией: δAux(xy) = x·δAux(y) + y·δAux(x) для генераторов x,y в кольце котант.
LaTeX
$$$$ \deltaAux\,(x y) = x \cdot (\deltaAux(y)) + y \cdot (\deltaAux(x)) $$$$
Lean4
theorem δAux_mul (x y) : δAux R Q (x * y) = x • (δAux R Q y) + y • (δAux R Q x) := by
induction x using MvPolynomial.induction_on' with
| monomial n r =>
induction y using MvPolynomial.induction_on' with
| monomial m
s =>
simp only [monomial_mul, δAux_monomial, Derivation.leibniz, tmul_add, tmul_smul, smul_tmul', Algebra.smul_def,
algebraMap_apply, aeval_monomial, mul_assoc]
rw [mul_comm (m.prod _) (n.prod _)]
simp only [pow_zero, implies_true, pow_add, Finsupp.prod_add_index']
| add y₁ y₂ hy₁ hy₂ => simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]; abel
| add x₁ x₂ hx₁ hx₂ => simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]; abel
