order_of (-1)

Stream: Is there code for X?

[Eric Rodriguez]

lemma one_eq_neg_iff {R} [ring R] [nontrivial R] : ring_char R = 2 ↔ (-1 : R) = 1 :=
begin
  rw ←not_iff_not,
  refine ⟨λ hr h1, _, λ h1 hr, _⟩,
  { rw [eq_comm, ←sub_eq_zero, sub_neg_eq_add] at h1,
    cases (ring_char R).eq_zero_or_pos with hrc hrc,
    { haveI := ring_char.eq_iff.mp hrc,
      haveI := char_p.char_p_to_char_zero R,
      apply @two_ne_zero' R,
      exact_mod_cast h1 },
    rw [show (1 + 1 : R) = (1 + 1 : ℕ), by norm_cast, show 1 + 1 = 2, from rfl] at h1,
    have := nat.le_of_dvd zero_lt_two (ring_char.dvd h1),
    interval_cases (ring_char R),
    { exact char_p.ring_char_ne_one h },
    { exact hr h } },
  { rw [eq_comm, ←sub_eq_zero, sub_neg_eq_add, show (1 + 1 : R) = (1 + 1 : ℕ), by norm_cast] at h1,
    apply h1,
    rw [ring_char.spec R, hr] }
end

instance fact_prime_two := fact.mk nat.prime_two

@[simp] lemma order_of_neg_one {R} [ring R] [nontrivial R] :
  order_of (-1 : R) = if ring_char R = 2 then 1 else 2 :=
begin
  split_ifs,
  { simpa [one_eq_neg_iff] using h },
  apply order_of_eq_prime,
  { simp },
  simpa [one_eq_neg_iff] using h
end

this cannot be the best way of doing this?!? do we have any of these results somewhere?

[Eric Wieser]

I think that first lemma is much easier than you have

[Yakov Pechersky]

I think Eric Wieser had the first lemma over arbitrary x, for the mp direction

[Eric Wieser]

I have a bunch of lemmas about characteristic 2 I should PR

[Yakov Pechersky]

Ah didn't even tag him!

[Eric Wieser]

From https://github.com/pygae/lean-ga/blob/68f3e4214dc0e13519170aad7c9aa691589149e3/src/geometric_algebra/from_mathlib/mathoverflow.lean#L167 there are a handful

[Eric Wieser]

Sorry, I meant https://github.com/eric-wieser/lean-ga/blob/bab185bad6c35b350678a58cb9ee55339a4927f7/src/geometric_algebra/from_mathlib/mathoverflow.lean#L165

[Eric Rodriguez]

mind if I PR them at some point? it was honestly a painful hour working with charp...

[Eric Wieser]

#60852 #10441

[Eric Wieser]

When you PR the iff versions later, you can use them to clean up docs#is_primitive_root.neg_one

[Eric Wieser]

Which seems to be the only lemma that mentions characteristic two

[Eric Rodriguez]

I added some machinery that makes order_of basically equivalent to is_primitive_root, so it should be super easy actually

[Eric Rodriguez]

I'm somewhat confused why they weren't unified earlier

[Riccardo Brasca]

It's probably only a psychological thing: even if I know that z : C is a primitive n-th root of unity if and only if its multiplicative order is n, in my mental image primitive roots is a ring related notion

[Riccardo Brasca]

Because we want to be able to say that r : R is a (primitive) root of unity, without knowing a priori that r is a unit

[Julian Külshammer]

But can't you say that? Since a refactor some months ago, order_of doesn't require to be in a group, so you can just express it as order_of r in the multiplicative group of R being positive without talking about units R.

[Eric Rodriguez]

Yes, this does currently work just fine