Theorems · Theorem · commutative algebra
Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R],
((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegralIf R is a Jacobson ring, and P is a maximal ideal of R[X],
then R → R[X]/P is an integral map.
- Defined in
- Mathlib.RingTheory.Jacobson.Ring
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites46
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- RingHomproof · cited by 10,189
- Top.topproof · cited by 9,680
- Polynomialstatement and proof · cited by 5,681
- Idealstatement and proof · cited by 4,748
- Bot.botproof · cited by 4,720
- HasQuotient.Quotientstatement and proof · cited by 2,301
- le_antisymmproof · cited by 2,068
- Polynomial.Cstatement and proof · cited by 1,598
- le_rflproof · cited by 1,558
- Polynomial.coeffproof · cited by 1,045
Cited by2
Results whose statement or proof uses this declaration.
- Polynomial.isMaximal_comap_C_of_isJacobsonRingproof · cited by 0
- Polynomial.comp_C_integral_of_surjective_of_isJacobsonRingproof · cited by 0