Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-13 17:08
f0cbe979
View on Github →
fix: minor changes to Analysis.Normed.Field.Basic from code review (
#2847
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Field/Basic.lean
deleted
theorem
Filter.IsBoundedUnder_le.mul_tendsto_zero
added
theorem
Filter.isBoundedUnder_le_mul_tendsto_zero