no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : n = 0
h : X ^ n - ↑C a = 0
⊢ ↑Multiset.card (nthRoots n a) ≤ n
simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - ↑C a = 0
⊢ degree (↑C (1 - a)) ≤ ↑0
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - ↑C a = 0
⊢ degree (X ^ n - ↑C a) ≤ ↑n
rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - ↑C a = 0
⊢ degree (↑C (1 - a)) ≤ ↑0
exact degree_C_le
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ ↑n
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑Multiset.card (nthRoots n a) ≤ n
rw [← WithBot.coe_le_coe]
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ ↑n
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ ↑n
simp only [← Nat.cast_withBot]
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ degree (X ^ n - ↑C a)
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ ↑n
rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(↑Multiset.card (nthRoots n a)) ≤ degree (X ^ n - ↑C a)
exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a)