coeff_rTensorAlgHom_tmul — Mathlib

English

For p ∈ MvPolynomial σ S ⊗_R N, the value rTensorAlgHom p equals rTensor p when viewed as linear maps; i.e., the two ways of forming the tensor-augmentation agree.

Русский

Для p в MvPolynomial σ S ⊗ N, отображение rTensorAlgHom p совпадает с rTensor p.

LaTeX

$$$rTensorAlgHom(p) = rTensor(p)$$$

Lean4

@[simp]
theorem coeff_rTensorAlgHom_tmul (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
    coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = (coeff d p) ⊗ₜ[R] n :=
  by
  rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
  rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply, Algebra.TensorProduct.includeRight_apply]
  rw [algebraMap_eq, mul_comm, coeff_C_mul]
  simp [mapAlgHom, coeff_map]

Похожие утверждения