English
A general Leibniz rule for products in the tensor setting: derivative of product is a sum of left and right multiplications of components with derivatives.
Русский
Обобщённое правило Лейбница для произведений в тензорном контексте: производная от произведения равна сумме левому и правому умножений на производные частей.
LaTeX
$$D.tensorProductTo (x * y) = TensorProduct.lmul' R x • D.tensorProductTo y + TensorProduct.lmul' R y • D.tensorProductTo x$$
Lean4
theorem tensorProductTo_mul (D : Derivation R S M) (x y : S ⊗[R] S) :
D.tensorProductTo (x * y) =
TensorProduct.lmul' (S := S) R x • D.tensorProductTo y + TensorProduct.lmul' (S := S) R y • D.tensorProductTo x :=
by
refine TensorProduct.induction_on x ?_ ?_ ?_
· rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]
swap
· intro x₁ y₁ h₁ h₂
rw [add_mul, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
intro x₁ x₂
refine TensorProduct.induction_on y ?_ ?_ ?_
· rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
swap
· intro x₁ y₁ h₁ h₂
rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
intro x y
simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo, TensorProduct.AlgebraTensorModule.lift_apply,
TensorProduct.lmul'_apply_tmul]
dsimp
rw [D.leibniz]
simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]
