Zulip Chat Archive

Stream: maths

Topic: X^k - X ≠ 0


view this post on Zulip 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
  admit
end

view this post on Zulip 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.

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

view this post on Zulip Alex J. Best (Jul 10 2020 at 20:11):

A couple of the rws should be a lemma

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jul 10 2020 at 21:00):

Almost certainly yes.

view this post on Zulip Patrick Massot (Jul 10 2020 at 21:00):

Go ahead

view this post on Zulip Alex J. Best (Jul 10 2020 at 21:14):

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


Last updated: May 12 2021 at 08:14 UTC