## Stream: maths

### Topic: X^k - X ≠ 0

#### Johan Commelin (Jul 10 2020 at 19:48):

What is the canonical way to prove

import data.polynomial

open polynomial

example (K : Type*) [ring K] [nontrivial K] (k : ℕ) (hk : 2 ≤ k) :
(X ^ k - X : polynomial K) ≠ 0 :=
begin
end


#### Johan Commelin (Jul 10 2020 at 19:49):

I can do it. But really, this should be a half-liner... and I haven't managed that yet.

#### Alex J. Best (Jul 10 2020 at 20:11):

example (K : Type*) [ring K] [nontrivial K] (k : ℕ) (hk : 2 ≤ k) :
(X ^ k - X : polynomial K) ≠ 0 :=
begin
apply ne_zero_of_degree_gt (_ : 1 < degree _),
end


#### Alex J. Best (Jul 10 2020 at 20:11):

A couple of the rws should be a lemma

#### Alex J. Best (Jul 10 2020 at 20:27):

Was this for the finite fields? Should I push it and a couple more slightly related lemmas to the branch?

#### Patrick Massot (Jul 10 2020 at 21:00):

Almost certainly yes.