Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 18:09 d75da1a2

View on Github →

feat(topology/algebra/group_with_zero): introduce has_continuous_inv' (#4804) Move lemmas about continuity of division from normed_field, add a few new lemmas, and introduce a new typeclass. Also use it for nnreals.

Estimated changes

deleted theorem continuous.div
deleted theorem continuous.inv'
deleted theorem continuous_at.div
deleted theorem continuous_at.inv'
deleted theorem continuous_on.div
deleted theorem continuous_on.inv'
deleted theorem continuous_within_at.div
deleted theorem continuous_within_at.inv'
deleted theorem filter.tendsto.div
deleted theorem filter.tendsto.div_const
deleted theorem filter.tendsto.inv'
deleted theorem normed_field.tendsto_inv
added theorem continuous.div
added theorem continuous.div_const
added theorem continuous.inv'
added theorem continuous_at.div
added theorem continuous_at.inv'
added theorem continuous_on.div
added theorem continuous_on.inv'
added theorem continuous_on_div
added theorem continuous_on_inv'
added theorem filter.tendsto.div
added theorem filter.tendsto.inv'
added theorem tendsto_inv'
deleted theorem nnreal.tendsto.sub
modified theorem nnreal.tendsto_coe