feat(Topology/Algebra/Group/Basic): add eq_of_tendsto_div_nhds_one (leanprover-community#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`.

Author: fernando-m-reich

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -1104,6 +1104,18 @@ theorem tendsto_div_nhds_one_iff {α : Type*} {l : Filter α} {x : G} {u : α 
   haveI A : Tendsto (fun _ : α => x) l (𝓝 x) := tendsto_const_nhds
   ⟨fun h => by simpa using h.mul A, fun h => by simpa using h.div' A⟩
 
+/-- If `f → a` and `g → b` along a nontrivial filter on the domain, valued in a
+Hausdorff topological group, then `f / g → 1` if and only if `a = b`. -/
+@[to_additive]
+theorem tendsto_div_nhds_one_iff_eq {α : Type*} {l : Filter α} [l.NeBot] [T2Space G]
+    {f g : α → G} {a b : G} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) :
+    Tendsto (fun x ↦ f x / g x) l (𝓝 1) ↔ a = b :=
+  ⟨fun hfg => tendsto_nhds_unique hf <| by simpa using hfg.mul hg,
+   fun h => by subst h; simpa using hf.div' hg⟩
+
+@[to_additive]
+alias ⟨eq_of_tendsto_div_nhds_one, _⟩ := tendsto_div_nhds_one_iff_eq
+
 @[to_additive]
 theorem nhds_translation_div (x : G) : comap (· / x) (𝓝 1) = 𝓝 x := by
   simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

Mathlib/Topology/Algebra/GroupWithZero.lean

@@ -192,6 +192,18 @@ theorem Filter.Tendsto.div {l : Filter α} {a b : G₀} (hf : Tendsto f l (𝓝
     (hg : Tendsto g l (𝓝 b)) (hy : b ≠ 0) : Tendsto (f / g) l (𝓝 (a / b)) := by
   simpa only [div_eq_mul_inv] using! hf.mul (hg.inv₀ hy)
 
+/-- If `f → a` and `g → b` along a nontrivial filter, valued in a Hausdorff
+`GroupWithZero` with continuous multiplication and `ContinuousInv₀`, and `b ≠ 0`,
+then `f / g → 1` if and only if `a = b`. -/
+theorem tendsto_div_nhds_one_iff_eq₀
+    {l : Filter α} [l.NeBot] [T2Space G₀] {a b : G₀}
+    (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) (hb : b ≠ 0) :
+    Tendsto (fun x ↦ f x / g x) l (𝓝 1) ↔ a = b :=
+  ⟨fun hfg => (div_eq_one_iff_eq hb).mp (tendsto_nhds_unique (hf.div hg hb) hfg),
+   fun hab => (div_eq_one_iff_eq hb).mpr hab ▸ hf.div hg hb⟩
+
+alias ⟨eq_of_tendsto_div_nhds_one₀, _⟩ := tendsto_div_nhds_one_iff_eq₀
+
 theorem Filter.tendsto_mul_iff_of_ne_zero [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀}
     (hg : Tendsto g l (𝓝 y)) (hy : y ≠ 0) :
     Tendsto (fun n => f n * g n) l (𝓝 <| x * y) ↔ Tendsto f l (𝓝 x) := by