supportedEquivMvPolynomial_symm_X

English

The inverse isomorphism sends the variable X i in MvPolynomial s R back to the corresponding variable X in MvPolynomial σ R, i.e. (supportedEquivMvPolynomial s).symm (X i) = X ↑i.

Русский

Обратное отображение изоморфизма переводит переменную X i из MvPolynomial s R обратно в переменную X в MvPolynomial σ R: (supportedEquivMvPolynomial s).symm (X i) = X ↑i.

LaTeX

$$$ (supportedEquivMvPolynomial s).symm (X i) = X \;(i).$$$

Lean4

@[simp]
theorem supportedEquivMvPolynomial_symm_X (s : Set σ) (i : s) :
    (↑((supportedEquivMvPolynomial s).symm (X i : MvPolynomial s R)) : MvPolynomial σ R) = X ↑i := by
  simp [supportedEquivMvPolynomial]

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