Mathlib Changelog
v4
Changelog
About
Github
Theorem
Filter.tendsto_inv_atBot_iff
Modification history
2025-03-18 23:10
Mathlib/Order/Filter/AtTopBot/Group.lean
chore(AtTopBot/Group): use `@[to_additive]` (#22461)
Added
Filter.tendsto_inv_atBot_iff
View on Github →