Convergence and squares near one

In a group with zero whose units form an open subspace, convergence to a nonzero element ensures that the quotient by that element is eventually a square, provided the squares in the unit group form a neighbourhood of one. Only separate continuity of multiplication is needed.

For commutative groups with zero, this preserves nonzero square classes under approximation.

theorem Filter.Tendsto.eventually_isSquare_div {X : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [TopologicalSpace G₀] [SeparatelyContinuousMul G₀] [IsOpenUnits G₀] {f : X → G₀} {l : Filter X} {a : G₀} (hf : Tendsto f l (nhds a)) (hsq : {u : G₀ˣ | IsSquare u} ∈ nhds 1) (ha : a ≠ 0) : ∀ᶠ (z : X) in l, f z ≠ 0 ∧ IsSquare (f z / a)

If the squares in the unit group of a group with zero form a neighbourhood of one, convergence to a nonzero element eventually gives nonzero values whose quotient by the limit is a square.