Theorems · Theorem · commutative algebra

RingHom.isIntegralElem_localization_at_leadingCoeff

∀ {R : Type u_5} {S : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
  (p : Polynomial R),
  Polynomial.eval₂ f x p = 0 →
    ∀ (M : Submonoid R),
      p.leadingCoeff ∈ M →
        ∀ {Rₘ : Type u_7} {Sₘ : Type u_8} [inst_2 : CommRing Rₘ] [inst_3 : CommRing Sₘ] [inst_4 : Algebra R Rₘ]
          [inst_5 : IsLocalization M Rₘ] [inst_6 : Algebra S Sₘ] [inst_7 : IsLocalization (Submonoid.map f M) Sₘ],
          (IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)

Defined in

Mathlib.RingTheory.Localization.Integral

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommRingCommRingAlgebraIsLocalizationAlgebraIsLocalization