equivMvPolynomial_symm_X — Mathlib

English

The inverse of the equivalence sends the indeterminate X_i to the canonical embedding ι_R M (b i).

Русский

Обратный환 эквивалентности отправляет переменную X_i в каноническое вложение ι_R M (b i).

LaTeX

$$$(\equivMvPolynomial b).symm( X_i ) = \iota_R M (b i)$$$

Lean4

@[simp]
theorem equivMvPolynomial_symm_X (b : Basis κ R M) (i : κ) :
    (equivMvPolynomial b).symm (MvPolynomial.X i) = ι R M (b i) :=
  (equivMvPolynomial b).toEquiv.symm_apply_eq.mpr <| equivMvPolynomial_ι_apply b i |>.symm

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