algebraTensorAlgEquiv_symm_map — Mathlib

English

The inverse under the isomorphism of algebraTensorAlgEquiv, applied to map(algebraMap_R_A) x, equals 1 ⊗ x.

Русский

Обратное отображение под изоморфизмом algebraTensorAlgEquiv, применённое к map(algebraMap_R_A) x, даёт 1 ⊗ x.

LaTeX

$$$ (algebraTensorAlgEquiv(R,A).symm (map (algebraMap R A) x)) = 1 \\otimes x $$$

Lean4

@[simp]
theorem algebraTensorAlgEquiv_symm_map (x : MvPolynomial σ R) :
    (algebraTensorAlgEquiv R A).symm (map (algebraMap R A) x) = 1 ⊗ₜ x :=
  DFunLike.congr_fun (algebraTensorAlgEquiv_symm_comp_aeval R A) x

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