mvPolynomialOptionEquivPolynomialAdjoin_C

English

Equality of trdeg under isomorphism for substructures as per AlgEquiv.

Русский

Равенство трансцендентной степени при изоморфизме подструктур в рамках AlgEquiv.

LaTeX

$$$\trdeg R A = \trdeg R A'$, при $e : A \cong_R A'$ $$

Lean4

theorem mvPolynomialOptionEquivPolynomialAdjoin_C (hx : AlgebraicIndependent R x) (r) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C (algebraMap _ _ r) := by simp

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