English
In a commutative group with zero and continuous division, if b ≠ 0, then Tendsto (f(k) / b) to (c / b) is equivalent to Tendsto f(k) to c.
Русский
В коммутативной группе с нулём и непрерывным делением, если b ≠ 0, тогда Tendsto (f(k)/b) к (c/b) эквивалентно Tendsto f(k) к c.
LaTeX
$$$b \neq 0 \implies \Big( \text{Tendsto}(f)_{l}(\mathcal{N}(c)) \iff \text{Tendsto}(f(k)/b)_{l}(\mathcal{N}(c/b)) \Big).$$$
Lean4
theorem tendsto_div_const_iff {G : Type*} [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G] {b : G}
(hb : b ≠ 0) {c : G} {f : α → G} {l : Filter α} : Tendsto (f · / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c) :=
by
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
convert h.div_const' b⁻¹ with k <;> rw [div_div, mul_inv_cancel₀ hb, div_one]
