α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : natDegree p ≠ 0
⊢ 0 ≤ B
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
⊢ natDegree p = 0
contrapose! hB
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
⊢ 0 ≤ B
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : natDegree p ≠ 0
⊢ 0 ≤ B
rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB
case intro
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
z : K
hz : z ∈ roots (map f p)
⊢ 0 ≤ B
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
⊢ 0 ≤ B
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
no goals
case intro
α : Type ?u.181042
R : Type ?u.181045
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_1
K : Type u_2
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
z : K
hz : z ∈ roots (map f p)
⊢ 0 ≤ B
exact le_trans (norm_nonneg _) (h3 z hz)