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