Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 09:37 cd41acab

View on Github →

Move tendsto_div to a better place

Estimated changes

Modified src/analysis/specific_limits.lean

added theorem tendsto_one_div_add_at_top_nhds_0_nat

Modified src/data/real/cau_seq_filter.lean

deleted theorem sequentially_complete.tendsto_div

Modified src/topology/sequences.lean