case h
α : Type u_5
E : Type u_4
F : Type u_2
G : Type ?u.7594842
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_1
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑(compLpL p μ (c • L)) f = ↑(c • compLpL p μ L) f
α : Type u_5
E : Type u_4
F : Type u_2
G : Type ?u.7594842
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_1
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
⊢ compLpL p μ (c • L) = c • compLpL p μ L
ext1 f
no goals
case h
α : Type u_5
E : Type u_4
F : Type u_2
G : Type ?u.7594842
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_1
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : { x // x ∈ Lp E p }
⊢ ↑(compLpL p μ (c • L)) f = ↑(c • compLpL p μ L) f
exact smul_compLp c L f