Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 13:04 17afc5c0

View on Github →

feat(topology/algebra/group_with_zero): continuity lemma for division (#9959)

  • This even applies when dividing by 0.
  • From the sphere eversion project.
  • This PR mentions filter.tendsto_prod_top_iff which is added by #9958

Estimated changes

added theorem filter.prod_top