Theorems · Theorem · commutative algebra
PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrime
∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime] {J : Ideal (PowerSeries R)},
J ≤ I →
PowerSeries.X ∉ I → J.FG → Ideal.map PowerSeries.constantCoeff I ≤ Ideal.map PowerSeries.constantCoeff J → I = J- Defined in
- Mathlib.RingTheory.PowerSeries.Ideal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIdeal.IsPrime
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites76
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Semiringproof · cited by 13,802
- RingHomstatement · cited by 10,189
- Submoduleproof · cited by 7,192
- Finset.sumproof · cited by 5,195
- Idealstatement and proof · cited by 4,748
- Set.rangeproof · cited by 4,705
- Finset.univproof · cited by 3,473
- one_mulproof · cited by 2,841
- Finset.sum_congrproof · cited by 2,323
Cited by1
Results whose statement or proof uses this declaration.
- PowerSeries.exist_eq_span_eq_ncard_of_X_notMemproof · cited by 2