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]