α : Type ?u.798282
E : α → Type ?u.798287
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
𝕜 : Type u_3
B : I → Type u_2
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp (k • 1) ⊤
α : Type ?u.798282
E : α → Type ?u.798287
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
𝕜 : Type u_3
B : I → Type u_2
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp (↑(algebraMap 𝕜 ((i : I) → B i)) k) ⊤
rw [Algebra.algebraMap_eq_smul_one]
no goals
α : Type ?u.798282
E : α → Type ?u.798287
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
𝕜 : Type u_3
B : I → Type u_2
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp (k • 1) ⊤
exact (one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)