Theorem PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime

Modification history

2025-11-19 16:14
Mathlib/RingTheory/PowerSeries/Ideal.lean
feat: power series over a noetherian ring is noetherian (#31149) …
Added PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrimeView on Github →