Theorems · Theorem · commutative algebra

IsLocalization.scaleRoots_commonDenom_mem_lifts

∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {Rₘ : Type u_3} [inst_1 : CommRing Rₘ] [inst_2 : Algebra R Rₘ]
  [inst_3 : IsLocalization M Rₘ] (p : Polynomial Rₘ),
  p.leadingCoeff ∈ (algebraMap R Rₘ).range →
    p.scaleRoots ((algebraMap R Rₘ) ↑(IsLocalization.commonDenom M p.support p.coeff)) ∈
      Polynomial.lifts (algebraMap R Rₘ)

Defined in: Mathlib.RingTheory.Localization.Integral
Cited by: 1 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites42

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapstatement and proof · cited by 4,706
Set.rangeproof · cited by 4,705
mul_oneproof · cited by 3,885
Submonoidstatement and proof · cited by 3,086
mul_commproof · cited by 2,262
mul_assocproof · cited by 1,667
MulZeroClass.zero_mulproof · cited by 1,625

Cited by1

Results whose statement or proof uses this declaration.

IsIntegral.exists_multiple_integral_of_isLocalizationproof · cited by 7