English
A further restatement of coeff for rTensorAlgHom applied to a tmul, confirming the coefficient structure.
Русский
Дополнительное утверждение о коэффициенте для rTensorAlgHom на tmul, подтверждающее структуру коэффициентов.
LaTeX
$$$coeff d (rTensorAlgHom (p \\otimes n)) = (coeff d p) \\otimes n$$$
Lean4
/-- The tensor product of a polynomial algebra by an algebra
is algebraically equivalent to a polynomial algebra -/
noncomputable def rTensorAlgEquiv : (MvPolynomial σ S) ⊗[R] N ≃ₐ[S] MvPolynomial σ (S ⊗[R] N) :=
by
apply AlgEquiv.ofLinearEquiv rTensor
· simp only [Algebra.TensorProduct.one_def]
apply symm
rw [← LinearEquiv.symm_apply_eq]
exact finsuppLeft_symm_apply_single (R := R) (0 : σ →₀ ℕ) (1 : S) (1 : N)
· intro x y
erw [← rTensorAlgHom_apply_eq (S := S)]
simp only [map_mul, rTensorAlgHom_apply_eq]
rfl
