polyEquivTensor_symm_apply_tmul_eq_smul

English

The inverse equivalence on a ⊗ p acts by smul: (polyEquivTensor R A).symm (a ⊗ p) = a • p.map(algebraMap R A).

Русский

Обратное отображение действует через умножение на скаляры: (polyEquivTensor R A).symm (a ⊗ p) = a • p.map(algebraMap R A).

LaTeX

$$(polyEquivTensor R A).symm (a ⊗ p) = a \\cdot p.map(\\mathrm{algebraMap}\\,R\\,A)$$

Lean4

@[simp]
theorem polyEquivTensor_symm_apply_tmul_eq_smul (a : A) (p : R[X]) :
    (polyEquivTensor R A).symm (a ⊗ₜ p) = a • p.map (algebraMap R A) :=
  rfl

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