distinguishing -1 : units int from 1

Stream: new members

[Antoine Chambert-Loir]

In the course of proving the simplicity of the alternating group, see
(The alternating group is simple!)[https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/The.20alternating.20group.20is.20simple!/near/266008041], I had to use a bunch of simple results which did not look automatic. I probably wrote more than necessary, but before I make a proper PR, the question is now to decide what to do with them.
So should the following be done at hand when needed (possibly simplified), or are they worth of inclusion into mathlib?

import tactic
import data.nat.parity

lemma neg_one_ne_one : (-1 : units ℤ) ≠ 1 :=
begin
  intro h,
  rw ← units.eq_iff at h,
  simpa only using h,
end

lemma even_pow_of_neg_one (n : ℕ) (hn : even n) :
  (-1 : units ℤ)^n = 1 :=
begin
  rw ← units.eq_iff,
  rw [units.coe_pow, units.coe_neg_one, units.coe_one],
  exact nat.neg_one_pow_of_even hn,
end

lemma odd_pow_of_neg_one (n : ℕ) (hn : odd n) :
  (-1 : units ℤ)^n = -1 :=
begin
  rw ← units.eq_iff,
  simp only [units.coe_one, units.coe_neg_one, units.coe_pow],
  exact nat.neg_one_pow_of_odd hn,
end

lemma pow_of_neg_one_is_one_of_even_iff (n : ℕ) :
  even n ↔ (-1 : units ℤ)^n = 1  :=
begin
  split,
  exact even_pow_of_neg_one n,

  intro h,
  rw  nat.even_iff_not_odd,
  intro h',
  apply neg_one_ne_one,
  rw ← odd_pow_of_neg_one n h', exact h,
end

lemma pow_of_neg_one_is_neg_one_of_odd_iff (n : ℕ) :
  odd n ↔ (-1 : units ℤ)^n = -1  :=
begin
  split,
  exact odd_pow_of_neg_one n,

  intro h,
  rw  nat.odd_iff_not_even,
  intro h',
  rw even_pow_of_neg_one n h' at h,
  apply neg_one_ne_one,
  exact h.symm,
 end

lemma neq_one_is_neg_one (u : units ℤ) (hu : u ≠ 1) : u = -1 :=
begin
    rw ← finset.mem_singleton,
    exact finset.mem_of_mem_insert_of_ne (finset.mem_univ u) hu,
end

[Eric Wieser]

The first one would be helped by docs#units.ne_iff, which is maybe worth having if it doesn't already exist

[Johan Commelin]

The first one should be dec_trivial, right?

[Johan Commelin]

Indeed

lemma neg_one_ne_one : (-1 : units ℤ) ≠ 1 :=
dec_trivial

works

[Eric Wieser]

How many of the lemmas above are true if you replace ℤ with some arbitrary ring?

[Antoine Chambert-Loir]

Most of them. And most of them only depend on -1 being an element of order 2 in a multiplicative group.

[Alex J. Best]

There are a few lemmas in mathlib already about units of int, like docs#int.units_eq_one_or docs#int.units_pow_eq_pow_mod_two

[Alex J. Best]

So hopefully they can be used to give some short proofs here, the odd/even things seem useful and I don't think I've seen them in mathlib

[Yakov Pechersky]

I've deal with the odd/even ones by destructing them into 2 * k + 1 or 2 * k

[Damiano Testa]

These are lemmas that work in a general ring:

import data.nat.parity

section general_ring
variables {R : Type*} [ring R]

lemma odd_pow_of_neg_one {n : ℕ} (hn : odd n) :
  (-1 : units R)^n = -1 :=
units.eq_iff.mp (by simpa using nat.neg_one_pow_of_odd hn)

lemma even_pow_of_neg_one {n : ℕ} (hn : even n) :
  (-1 : units R)^n = 1 :=
units.eq_iff.mp (by simpa using nat.neg_one_pow_of_even hn)

end general_ring

[Damiano Testa]

and the last lemma also works with dec_trivial!:

lemma neq_one_is_neg_one {u : units ℤ} (hu : u ≠ 1) : u = -1 :=
by dec_trivial!

[Andrew Yang]

I also needed some -1 ^ n stuff recently, and I have these in a branch of mine.

import data.int.parity
namespace int
variables (n m : ℤ)

def neg_one_pow (n : ℤ) : ℤ := @has_pow.pow (units ℤ) ℤ _ (-1) n
example : neg_one_pow 1 = -1 := rfl
example : neg_one_pow (-1) = -1 := rfl
example : neg_one_pow 0 = 1 := rfl
example : neg_one_pow (n + m) = neg_one_pow n * neg_one_pow m := sorry
example : neg_one_pow n = if even n then 1 else -1 := sorry
example : neg_one_pow n = (-1) ^ n.nat_abs := sorry
example (n : ℕ) : neg_one_pow n = (-1) ^ n := sorry
example : neg_one_pow (-n) = neg_one_pow n := sorry
example : neg_one_pow (n - m) = neg_one_pow n * neg_one_pow m := sorry
example : neg_one_pow n * neg_one_pow n = 1 := sorry
example {α : Type*} [add_comm_group α] (n : ℤ) (X : α) :
  neg_one_pow n • neg_one_pow n • X = X := sorry

end int

If someone is making a pr about this, it would be great if these stuff are included :thank_you:

[Antoine Chambert-Loir]

I also understood from @Riccardo Brasca that he had needed some (-1)^n stuff as well.

[Antoine Chambert-Loir]

Additional stylistic question: is it useful to make n as much implicit as possible ?

[Yakov Pechersky]

n should be implicit for your iffs. in the case of implications, if n is mentioned in a different hypothesis, you may make it implicit. but i find that it is often more clunky to have it implicit, I might say rw <-odd_pow_of_neg_one 3 which then leaves me with a nice side goal of odd 3. I like that more than trying to prove odd 3 first.

[Eric Rodriguez]

I had some proof that (-1) has order 2 iff not char 2 or trivial somewhere if that's helpful

[Eric Rodriguez]

I think algebra/char_two/basic

[Eric Wieser]

I think we're also missing:

example {n : ℕ} (hn : odd n) (u : units R) :
  (-u : units R)^n = -(u^n) :=
sorry

The general problem is that docs#units.has_neg satisfies no stronger typeclasses, so every neg lemma has to be restated about it

[Riccardo Brasca]

In flt-regular we had to work with something like (-1)^(n*(n-1)/2) and the problem was rather integer division if I remember correctly

[Johan Commelin]

I think it makes sense to have a dedicated function ℤ → R that maps even integers to 1 and odd integers to -1.

[Johan Commelin]

Writing (-1)^n is common notation in informal maths, but it's maybe not the optimal way of encoding it in Lean.

[Antoine Chambert-Loir]

Such a function would make sense in standard math — look at how quadratic reciprocity is usually stated : $(-1)^{(p-1)(q-1)/2}$ is only natural once people have digested it as “if $p$ and $q$ are both 3 mod 4, then $-1$, else $1$”.

[Johan Commelin]

Yep, I agree.

[Johan Commelin]

Well, but would foo ((p-1)*(q-1)/2) be easier to parse?

[Antoine Chambert-Loir]

Not much, I agree. One even needs more…

[Johan Commelin]

Note that in mathlib you can write (-1)^(p*q/2) and get the same answer. The joys of integer division...

[Riccardo Brasca]

I totally agree, I've never understood why people state quadratic reciprocity in that way.

[Kevin Buzzard]

Yes! The (p-1)(q-1)/2 is a fabulous obfuscation, as is (p^2-1)/8 for the case of (2/p)

[Johan Commelin]

@Andrew Yang would you mind PRing your (-1)^n stuff?

[Andrew Yang]

#11204

[Johan Commelin]

Thanks!