English
The linear map toFunLinear respects multiplication on simple tensors: applying toFunLinear to (a1 a2) ⊗ (p1 p2) equals the product of toFunLinear(a1 ⊗ p1) and toFunLinear(a2 ⊗ p2) in A[X].
Русский
Линейное отображение toFunLinear сохраняет умножение на простых тензорах: toFunLinear((a1 a2) ⊗ (p1 p2)) = toFunLinear(a1 ⊗ p1) · toFunLinear(a2 ⊗ p2) в A[X].
LaTeX
$$$(toFunLinear_R A)((a_1 a_2) \\otimes (p_1 p_2)) = (toFunLinear_R A)(a_1 \\otimes p_1) \\cdot (toFunLinear_R A)(a_2 \\otimes p_2)$$$
Lean4
theorem toFunLinear_mul_tmul_mul (a₁ a₂ : A) (p₁ p₂ : R[X]) :
(toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂) :=
by
classical
simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
ext k
simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]
conv_rhs => rw [coeff_mul]
simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite, mul_zero, ite_mul,
zero_mul]
simp_rw [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]
simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]
