algebraTensorAlgEquiv_tmul — Mathlib

English

For a ∈ A and p ∈ MvPolynomial(σ, R), the canonical isomorphism sends a ⊗ p to a · map(algebraMap_R_A)(p).

Русский

Для a ∈ A и p ∈ MvPolynomial(σ, R) канонический изоморфизм отправляет a ⊗ p в a · map(algebraMap_R_A)(p).

LaTeX

$$$ algebraTensorAlgEquiv(R,A)(a \\otimes p) = a \\cdot MvPolynomial.map(\\mathrm{algebraMap}\,R\,A)\,p $$$

Lean4

@[simp]
theorem algebraTensorAlgEquiv_tmul (a : A) (p : MvPolynomial σ R) :
    algebraTensorAlgEquiv R A (a ⊗ₜ p) = a • MvPolynomial.map (algebraMap R A) p :=
  by
  simp [algebraTensorAlgEquiv, Algebra.smul_def]
  rfl

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