Theorems · Theorem · commutative algebra
PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime
∀ {R : Type u_1} [inst : CommRing R] {P : Ideal (PowerSeries R)} [P.IsPrime],
Submodule.spanFinrank P ≤ Submodule.spanFinrank (Ideal.map PowerSeries.constantCoeff P) + 1- Defined in
- Mathlib.RingTheory.PowerSeries.Ideal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 108 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.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement · cited by 10,189
- Idealstatement and proof · cited by 4,748
- le_transproof · cited by 985
- Ideal.IsPrimestatement and proof · cited by 827
- PowerSeriesstatement and proof · cited by 797
- Ideal.mapstatement and proof · cited by 692
- Eq.leproof · cited by 605
- PowerSeries.Xproof · cited by 183
- PowerSeries.constantCoeffstatement and proof · cited by 126
- Ideal.FGproof · cited by 99
- Submodule.spanFinrankstatement and proof · cited by 49
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.