Commit 2025-03-18 23:10 3d8165ea

View on Github →

chore(AtTopBot/Group): use @[to_additive] (#22461)

Estimated changes

deleted theorem Filter.comap_abs_atTop
added theorem Filter.comap_inv_atBot
added theorem Filter.comap_inv_atTop
deleted theorem Filter.comap_neg_atBot
deleted theorem Filter.comap_neg_atTop
added theorem Filter.map_inv_atBot
added theorem Filter.map_inv_atTop
deleted theorem Filter.map_neg_atBot
deleted theorem Filter.map_neg_atTop