no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (↑(expand R (p ^ Nat.zero)) f)
⊢ Irreducible f
rwa [pow_zero, expand_one] at hf
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p * p ^ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p ^ Nat.succ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
rw [pow_succ] at hf
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p * p ^ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
rwa [expand_expand]