case zero
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f

case prime
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f
cases hF
no goals
case zero
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩
no goals
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ ↑(expand F (1 ^ 0)) f = f
rw [pow_zero, expand_one]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : Separable g
hge : ↑(expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f
case prime
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
no goals
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : Separable g
hge : ↑(expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f
exact ⟨g, hgs, n, hge⟩