isTheta_const_mul_left — Mathlib

English

Inverse-Theta equivalence: the IsTheta equivalence of inverses implies the original IsTheta equivalence, under appropriate normed field assumptions.

Русский

Эквивалентность Θ для обратных функций повторно отражает исходную Θ-эквивалентность.

LaTeX

$$$ (f =Θ[l] g) \Rightarrow ((f)^{-1} =Θ[l] (g)^{-1}) $.$$

Lean4

theorem isTheta_const_mul_left {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) : (fun x ↦ c * f x) =Θ[l] g ↔ f =Θ[l] g := by
  simpa only [← smul_eq_mul] using isTheta_const_smul_left hc

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