zpow — Mathlib

English

If c ≠ 0 in a normed field and f' and g are functions with f' =Θ_l g, then the function x ↦ c · f'(x) is Θ_l g if and only if f' is Θ_l g.

Русский

Если c ≠ 0 в нормированном поле, и f' =Θ_l g, то x ↦ c · f'(x) имеет Θ-отношение к g тогда и только тогда, когда f' =Θ_l g.

LaTeX

$$$ c \neq 0 \Rightarrow (\, (x \mapsto c \cdot f'(x)) =Θ[l] g \iff f'(x) =Θ[l] g). $$$

Lean4

theorem zpow {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℤ) : (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n :=
  by
  cases n
  · simpa only [Int.ofNat_eq_coe, zpow_natCast] using h.pow _
  · simpa only [zpow_negSucc] using (h.pow _).inv

Похожие утверждения