supportedEquivMvPolynomial_symm_C

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]

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