smul_iff — Mathlib

English

For hc ≠ 0, MemHolder r (c • f) is equivalent to MemHolder r f.

Русский

Для hc ≠ 0, MemHolder r (c • f) эквивалентно MemHolder r f.

LaTeX

$$$\|c\|_+ \neq 0 \Rightarrow (\operatorname{MemHolder}(r, c\cdot f) \iff \operatorname{MemHolder}(r,f)).$$$

Lean4

theorem smul_iff {𝕜} [SeminormedRing 𝕜] [Module 𝕜 Y] [NormSMulClass 𝕜 Y] {c : 𝕜} (hc : ‖c‖₊ ≠ 0) :
    MemHolder r (c • f) ↔ MemHolder r f :=
  by
  refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩
  rw [← HolderWith.smul_iff _ hc, inv_mul_cancel_right₀ hc]
  exact hh

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