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






leanprover-community/mathlib,leanprover-community/mathlib