α : Type ?u.177157
R : Type u_1
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff (↑C (coeff p 0)) 0) (↑C (coeff p 0))‖ ≤ ‖eval y (↑C (coeff p 0))‖
α : Type ?u.177157
R : Type u_1
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff p 0) p‖ ≤ ‖eval y p‖
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]
no goals
α : Type ?u.177157
R : Type u_1
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff (↑C (coeff p 0)) 0) (↑C (coeff p 0))‖ ≤ ‖eval y (↑C (coeff p 0))‖
simp