Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 19:19 1f11f3f3

View on Github →

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

Estimated changes

deleted theorem filter.eventually_eq.div'
modified theorem filter.eventually_eq.div
deleted theorem filter.eventually_eq.sub