mathlib
1f11f3f3 - chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952)

Commit
3 years ago
chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952)
Author
Parents
Loading