X^k - X ≠ 0

Stream: maths

[Johan Commelin]

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
  admit
end

[Johan Commelin]

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

[Alex J. Best]

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 _),
  rw [sub_eq_add_neg, add_comm, degree_add_eq_of_degree_lt]; simp; exact_mod_cast hk,
end

[Alex J. Best]

A couple of the rws should be a lemma

[Alex J. Best]

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

[Patrick Massot]

Almost certainly yes.

[Patrick Massot]

Go ahead

[Alex J. Best]

Already did, I was just worried I'd push over Johan as he was leaving!