Theorem HahnSeries.order_le_of_coeff_ne_zero

Modification history

2025-12-11 08:08
Mathlib/RingTheory/HahnSeries/Basic.lean
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …
Modified HahnSeries.order_le_of_coeff_ne_zeroView on Github →
2025-04-11 17:23
Mathlib/RingTheory/HahnSeries/Basic.lean
feat: generalize rest of Mathlib.RingTheory (#23194) …
Modified HahnSeries.order_le_of_coeff_ne_zeroView on Github →
2024-08-17 12:07
Mathlib/RingTheory/HahnSeries/Basic.lean
chore (Data.Multiset.Basic): avoid bundled ordered algebra for basic results on multisets (#14477) …
Modified HahnSeries.order_le_of_coeff_ne_zeroView on Github →
2024-02-16 04:51
Mathlib/RingTheory/HahnSeries.lean
chore: Split HahnSeries file (#10595) …
Modified HahnSeries.order_le_of_coeff_ne_zeroView on Github →
2023-05-23 12:52
Mathlib/RingTheory/HahnSeries.lean
feat: port RingTheory.HahnSeries (#4261)
Added HahnSeries.order_le_of_coeff_ne_zeroView on Github →