no goals
α : Type u_1
β : Type ?u.107793
γ : Type ?u.107796
ι : Type ?u.107799
inst✝ : SeminormedRing α
⊢ ‖↑0‖ ≤ ↑0 * ‖1‖
simp
α : Type u_1
β : Type ?u.107793
γ : Type ?u.107796
ι : Type ?u.107799
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
α : Type u_1
β : Type ?u.107793
γ : Type ?u.107796
ι : Type ?u.107799
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑(n + 1)‖ ≤ ↑(n + 1) * ‖1‖
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
no goals
α : Type u_1
β : Type ?u.107793
γ : Type ?u.107796
ι : Type ?u.107799
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl