R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ 1 ≠ 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ rootSet (X ^ n) S = {0}
rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ 1 ≠ 0
exact one_ne_zero