no goals
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei✝ : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁹ : Fintype ι
inst✝¹⁸ : Fintype ι'
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹⁴ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝¹² : (i : ι') → NormedAddCommGroup (E' i)
inst✝¹¹ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝¹⁰ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei✝ i)
inst✝⁹ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei✝ i)
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜 G'
c : 𝕜
f✝ g : ContinuousMultilinearMap 𝕜 E G
m✝ : (i : ι) → E i
𝕜' : Type ?u.527868
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace 𝕜' G
inst✝² : SMulCommClass 𝕜 𝕜' G
Ei : Fin n → Type u_1
inst✝¹ : (i : Fin n) → NormedAddCommGroup (Ei i)
inst✝ : (i : Fin n) → NormedSpace 𝕜 (Ei i)
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i
b : ℝ
hm : ‖m‖ ≤ b
⊢ ‖↑f m‖ ≤ ‖f‖ * b ^ n
simpa only [Fintype.card_fin] using
  f.le_op_norm_mul_pow_card_of_le m fun i => (norm_le_pi_norm m i).trans hm