Commit 2026-07-17 21:13 f0c0e38c

feat(Topology/Algebra/Group/Basic): add eq_of_tendsto_div_nhds_one (#41230) Adds tendsto_div_nhds_one_iff_eq to Topology.Algebra.Group.Basic, next to tendsto_div_nhds_one_iff: for functions into a Hausdorff topological group, if f → a and g → b along a nontrivial filter, then f / g → 1 if and only if a = b. The implication eq_of_tendsto_div_nhds_one is kept as an alias, and the additive versions are generated by @[to_additive]. Also adds the GroupWithZero/ContinuousInv₀ variant tendsto_div_nhds_one_iff_eq₀ (assuming b ≠ 0), with its implication alias eq_of_tendsto_div_nhds_one₀, in Topology.Algebra.GroupWithZero.