not_dvd_pow_sub_one

Stream: Is there code for X?

[Bolton Bailey]

Is there code for this?

theorem not_dvd_pow_sub_one (p n: ℕ) (hn : 0 < n) (hp : 2 ≤ p) (hnp : p ∣ p ^ n - 1) : False :=

[Kevin Buzzard]

I don't like the look of statements which involve natural subtraction. How did you even end up with that as a hypothesis? I should think a % p = b % p is a better way of saying "p divides a - b and by the way I can prove a>=b".

[Bolton Bailey]

The minus one comes from docs#Fintype.card_units

[Bolton Bailey]

The theorem I am ultimately trying to prove is that the subgroup of units of a field, cast to the field, is not zero, here is what I have:

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Subgroup.Finite
import Mathlib.Data.Polynomial.Eval
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.FieldTheory.Finite.Basic

open scoped BigOperators Classical


theorem not_dvd_pow_sub_one (p n: ℕ) (hn : 0 < n) (hp : 2 ≤ p) (hnp : p ∣ p ^ n - 1) : False :=
by
  have ⟨k, hk⟩ := foobar n hn
  rw [hk] at hnp
  simp at hnp
  rw [pow_add] at hnp
  simp at hnp
  -- exact
-- aesop
  rw [Nat.dvd_iff_mod_eq_zero] at hnp
  rw [Nat.sub_mod]
  have foo : 1 ≤ p ^ n := by sorry
  zify [foo] at hnp hp
  rw [Int.sub_emod] at hnp
  -- simp at hnp
  rw [foob (p : ℤ) n hn] at hnp
  simp only [zero_sub, dvd_neg] at hnp
  simp only [-EuclideanDomain.mod_eq_zero, hp] at hnp -- This should simplify the
  rw [@Int.emod_eq_of_lt 1 (p : ℤ) _ _]
  sorry


theorem subgroup_of_units_card_ne_zero {F : Type} [Field F] [Fintype F]
    (G : Subgroup (Units (F))) : (Fintype.card G : F) ≠ 0 :=
  by
  -- Group of units of a finite field of order p^n is p^n-1
  have ⟨p, char_p⟩ := CharP.exists F
  have ⟨n, hp, hnp⟩ := FiniteField.card F p
  have card_units_F := @Fintype.card_units F _ _ _
  rw [hnp] at card_units_F
  -- As a subgroup, G's card must divide this
  have hl := Subgroup.card_subgroup_dvd_card G
  rw [card_units_F] at hl
  -- To equal zero when cast to field, subgroup card must be multiple of p
  intro heq0
  rw [(charP_iff F p).mp char_p] at heq0
  -- This implies p ∣ p^n - 1
  have hdvd := dvd_trans heq0 hl
  unfold PNat.val at hdvd
  clear heq0 hl card_units_F hnp char_p G
  -- This should lead to a contradiction, but this is hard to prove in lean due to tsub hell
  apply not_dvd_pow_sub_one p n.val
  exact PNat.pos n
  exact Nat.Prime.two_le hp
  exact hdvd

[Bolton Bailey]

What I think I want to do is move to the integers mod p and simplify, is there a standard way to convert a statement a % p = 0 into "a cast to Zmod p" = 0

[Bolton Bailey]

Ok I've got it down to something much simpler

theorem not_dvd_of_lt (p : ℤ) (h : 1 < p) : ¬ p ∣ 1 := by
  exact?

Is this somewhere? Edit: managed to solve this via Int.mod_eq_of_lt

[Kevin Buzzard]

Bolton Bailey said:

The minus one comes from docs#Fintype.card_units

I think that it would be better to write that lemma as card(units) + 1 = card(thing). Note that a+1=b implies b-1=a but not the other way around, so my suggestion is a better lemma.

[Bolton Bailey]

Ok, but then how am I supposed to apply transitivity of divisibility?

[Kevin Buzzard]

you can still talk about p divides a or p divides b, you just are in better shape because there's no natural subtraction

[Bolton Bailey]

I'm still confused. The crux of my proof is that p | card G and card G | p^n - 1, so there's a contradiction. I'm not even sure how I express the second one without nat subtraction.

[Bolton Bailey]

Hmm, I guess the idea is that I use p | card G and card G | card (Units F) to prove p | card (Units F), and then I also have p | card F <-> p | card (Units F) + 1 and then I somehow show that a number greater than 1 can't divide k and k+1 at the same time?

[Kevin Buzzard]

theorem not_dvd_pow_sub_one (p n: ℕ) (hn : 0 < n) (hp : 2 ≤ p) (hnp : p ∣ p ^ n - 1) : False :=
by
  rw [← Nat.modEq_iff_dvd' (one_le_pow_of_one_le (by linarith) n)] at hnp -- no more nat subtraction
  have := dvd_pow_self p hn.ne'
  rw [← Nat.modEq_zero_iff_dvd] at this
  refine Nat.zero_ne_one $ Nat.ModEq.eq_of_abs_lt (hnp.trans this).symm (?_ : (1 : ℤ) < p)
  exact_mod_cast hp

[Bolton Bailey]

After seeing how this can still be proved without tsub, I think I agree that card_units would be better off expressed in terms of add. Maybe the biggest objection is the aesthetics: I feel for some reason like I am more used to expressing this theorem the way it's currently written, maybe because I think of totient p as being p-1 for prime p (docs#Nat.totient_prime also seems to use tsub). At the very least, there should be primed versions of these lemmas to express them without tsub.

[Yury G. Kudryashov]

Here is a proof with nat subtraction:

import Mathlib.Data.Nat.Order.Lemmas
import Mathlib.Data.Nat.Pow

theorem not_dvd_pow_sub_one (p n: ℕ) (hn : 0 < n) (hp : 2 ≤ p) (hnp : p ∣ p ^ n - 1) : False := by
  have : ¬(p ∣ 1) := mt Nat.dvd_one.1 <| ne_of_gt hp
  rw [Nat.dvd_add_iff_right hnp, Nat.sub_add_cancel] at this
  exacts [this (dvd_pow_self _ hn.ne'), Nat.one_le_pow _ _ <| lt_of_lt_of_le two_pos hp]

[Jz Pan]

I have a question on your subgroup_of_units_card_ne_zero. Since G is a group, it must contains 1 whose image in F is also 1. So I think (Fintype.card G : F) ≠ 0 is trivial?

[Kyle Miller]

@Jz Pan What if card F | card G? (It's clear that card G itself is not zero, but not that it's nonzero as an element of F.)

[Jz Pan]

Sorry I am confused by the theorem name. So you mean the characteristic of F does not divide the size of G. I got it.