no goals
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a : α
x✝ : [a] ≠ []
⊢ ‖prod [a]‖ ≤ prod (map norm [a])
simp
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * prod (b :: l)‖ ≤ ‖a‖ * prod (map norm (b :: l))
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (a :: b :: l)‖ ≤ prod (map norm (a :: b :: l))
rw [List.map_cons, List.prod_cons, @List.prod_cons _ _ _ ‖a‖]
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (b :: l)‖ ≤ prod (map norm (b :: l))
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * prod (b :: l)‖ ≤ ‖a‖ * prod (map norm (b :: l))
refine' le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left _ (norm_nonneg _))
no goals
α : Type u_1
β : Type ?u.110463
γ : Type ?u.110466
ι : Type ?u.110469
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (b :: l)‖ ≤ prod (map norm (b :: l))
exact List.norm_prod_le' (List.cons_ne_nil b l)