English
The inverse of the isomorphism sends the constant polynomial C x to the corresponding algebra element in the subalgebra, i.e. (supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x.
Русский
Обратное отображение изоморфизма отправляет константный многочлен C x в соответствующий элемент подалгебры: (supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x.
LaTeX
$$$ (supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x $$$
Lean4
@[simp]
theorem supportedEquivMvPolynomial_symm_C (s : Set σ) (x : R) :
(supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x :=
by
ext1
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]