Commit 2026-02-16 15:42 8cf8a74b

View on Github →

feat: review lemmas about tendsto and group operations (#34792)

  • Add Filter.tendsto_mul_const_iff, Filter.tendsto_const_mul_iff and Filter.tendsto_div_const_iff'.
  • prime Filter.tendsto_const_div_iff (since it's about Group not GroupWithZero
  • Generalize a few results to nonabelian groups. In Filter.tendsto_const_div_iff this required changing ContinuousDiv to IsTopologicalGroup (which is actually equivalent for groups).

Estimated changes