Theorems · Definition · commutative algebra

StandardEtalePair.equivMvPolynomialQuotient

{R : Type u_1} →
  [inst : CommRing R] →
    (P : StandardEtalePair R) →
      P.Ring ≃ₐ[R]
        MvPolynomial (Fin 2) R ⧸
          Ideal.span
            {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
              (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}

R[X][Y]/⟨f, Yg-1⟩ ≃ R[X, Y]/⟨f, Yg-1⟩

Defined in

Mathlib.RingTheory.Etale.StandardEtale

Cited by

3 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing