Theorem PowerSeries.X_eq_normalizeX

Modification history

2024-07-05 11:29
Mathlib/RingTheory/PowerSeries/Inverse.lean
feat: add properties of the X-adic valuation on `PowerSeries K` (#13064) …
Modified PowerSeries.X_eq_normalizeXView on Github →
2024-05-21 11:42
Mathlib/RingTheory/PowerSeries/Inverse.lean
feat(RingTheory/PowerSeries/Inverse): add two lemmas on the normalization of `(X : PowerSeries k)` (#13063) …
Added PowerSeries.X_eq_normalizeXView on Github →