equivMvPolynomial_ι_apply — Mathlib

English

Under the equivalence, the image of the canonical injection ι_R M (b i) corresponds to the indeterminate X_i in MvPolynomial κ R.

Русский

При помощи эквивалентности образ канонического вложения ι_R M (b i) соответствует переменной X_i в MvPolynomial κ R.

LaTeX

$$$\equivMvPolynomial\;b\, (\iota_R M (b i)) = X_i$$$

Lean4

@[simp]
theorem equivMvPolynomial_ι_apply (b : Basis κ R M) (i : κ) : equivMvPolynomial b (ι R M (b i)) = .X (R := R) i :=
  (SymmetricAlgebra.lift_ι_apply _ _).trans <| by simp

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