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_1
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : NormedSpace 𝕜' G
inst✝² : IsScalarTower 𝕜' 𝕜 G
inst✝¹ : (i : ι) → NormedSpace 𝕜' (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
⊢ ‖restrictScalars 𝕜' f‖ = ‖f‖
simp only [norm_def, coe_restrictScalars]