𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.338526
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.338621
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.338711
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
⊢ IsBoundedBilinearMap 𝕜 fun p => p.fst • p.snd
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.338526
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.338621
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.338711
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
⊢ IsBoundedBilinearMap 𝕜 fun p => p.fst * p.snd
simp_rw [← smul_eq_mul]
no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.338526
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.338621
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.338711
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
⊢ IsBoundedBilinearMap 𝕜 fun p => p.fst • p.snd
exact isBoundedBilinearMap_smul