Theorem HahnSeries.leadingCoeff_neg_iff

Modification history

2025-12-11 08:08
Mathlib/RingTheory/HahnSeries/Lex.lean
chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …
Modified HahnSeries.leadingCoeff_neg_iffView on Github →
2025-06-16 07:16
Mathlib/RingTheory/HahnSeries/Lex.lean
feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (#25168) …
Added HahnSeries.leadingCoeff_neg_iffView on Github →