Zulip Chat Archive

Stream: new members

Topic: distinguishing -1 : units int from 1


Antoine Chambert-Loir (Dec 28 2021 at 11:54):

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 (Dec 28 2021 at 13:19):

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

Johan Commelin (Dec 28 2021 at 13:22):

The first one should be dec_trivial, right?

Johan Commelin (Dec 28 2021 at 13:23):

Indeed

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

works

Eric Wieser (Dec 28 2021 at 13:24):

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

Antoine Chambert-Loir (Dec 28 2021 at 13:25):

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

Alex J. Best (Dec 28 2021 at 13:27):

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 (Dec 28 2021 at 13:28):

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 (Dec 28 2021 at 13:31):

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

Damiano Testa (Dec 28 2021 at 13:33):

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 (Dec 28 2021 at 13:35):

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 (Dec 28 2021 at 13:36):

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 (Dec 28 2021 at 13:37):

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

Antoine Chambert-Loir (Dec 28 2021 at 13:38):

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

Yakov Pechersky (Dec 28 2021 at 13:41):

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 (Dec 28 2021 at 14:32):

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

Eric Rodriguez (Dec 28 2021 at 14:32):

I think algebra/char_two/basic

Eric Wieser (Dec 28 2021 at 15:06):

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 (Dec 28 2021 at 15:18):

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 (Dec 28 2021 at 15:25):

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

Johan Commelin (Dec 28 2021 at 15:26):

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 (Dec 28 2021 at 15:28):

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 (Dec 28 2021 at 15:29):

Yep, I agree.

Johan Commelin (Dec 28 2021 at 15:30):

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

Antoine Chambert-Loir (Dec 28 2021 at 15:34):

Not much, I agree. One even needs more…

Johan Commelin (Dec 28 2021 at 15:36):

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

Riccardo Brasca (Dec 28 2021 at 16:06):

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

Kevin Buzzard (Dec 28 2021 at 23:17):

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 (Jan 03 2022 at 12:33):

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

Andrew Yang (Jan 03 2022 at 14:18):

#11204

Johan Commelin (Jan 03 2022 at 14:21):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC