Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-12-31 16:08
0e87cb2c
View on Github →
feat(Normed/Group): add
tendsto_norm_div_self_nhdsGE
(
#20311
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
added
theorem
tendsto_norm_div_self_nhdsGE