Commit 2026-01-19 18:13 53871e28

View on Github →

feat(RingTheory/HahnSeries): generalise IsDomain instance (#34147)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean

added theorem Finset.prod_eq_prod_iff_single

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

deleted theorem mul_eq_mul_left_iff

deleted theorem mul_eq_mul_right_iff

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

added theorem mul_eq_mul_left_iff

added theorem mul_eq_mul_right_iff

modified theorem mul_left_inj'

modified theorem mul_right_inj'

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

modified theorem HahnSeries.order_mul

modified theorem HahnSeries.order_pow