Commit 2026-01-02 22:26 c3a9c0bd

View on Github →

feat: IsStrictOrderedRing (Lex R⟦Γ⟧) (#33398) Used in the CGT repo.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Lex.lean

modified theorem HahnSeries.leadingCoeff_nonneg_iff

modified theorem HahnSeries.leadingCoeff_nonpos_iff

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.leadingCoeff_mul

added theorem HahnSeries.leadingCoeff_mul_of_ne_zero

deleted theorem HahnSeries.leadingCoeff_mul_of_nonzero

added theorem HahnSeries.orderTop_mul

added theorem HahnSeries.orderTop_mul_of_ne_zero

deleted theorem HahnSeries.orderTop_mul_of_nonzero

added theorem HahnSeries.order_mul_of_ne_zero

deleted theorem HahnSeries.order_mul_of_nonzero