question regarding proof about wreath product

Stream: new members

[Francisco Silva]

Hello. I'm new to Lean and I have been trying to implement the regular wreath product to learn it.
I have proved that a Sylow $p$-subgroup of $S_{p^n}$ is the iterated wreath product of $n$ copies of $Z_p$.
I have uploaded what I have done here: https://github.com/ciskiko/lean-proj/blob/main/RegularWreathProduct.lean

One of the parts of the proof consists in a cardinality argument. I defined the function mu:

def mu (p:ℕ) : ℕ → ℕ
  | 0 => 0
  | n+1 => p * mu p n + 1

And I want to prove the lemma lemma mu_succ' {p n :ℕ} [NeZero p]: mu p (n+1) = p^n + mu p n.
I managed to do it in a very convoluted way, however I imagine there is some simpler way. This is basically Legendre's formula applied to a prime power, but I don't think it has been added to mathlib.

Another question: is there a simple way to implement the trivial group? I used Unitwith a group instance but it seems too complicated for such a basic concept.

[Matt Diamond]

re: the trivial group, there's already an abelian group instance defined for PUnit (which is the universe-polymorphic Unit) via docs#PUnit.commGroup, so you can use that without needing to define the group instance yourself

[Kevin Buzzard]

Why not just define

open Finset
def mu' (p n : ℕ) : ℕ := ∑ i ∈ range n, p ^ i

rather than doing everything from scratch? Then the proof will be much easier.

[Kevin Buzzard]

import Mathlib

open Finset
def mu' (p n : ℕ) : ℕ := ∑ i ∈ range n, p ^ i

lemma mu'_def (p n : ℕ) : mu' p n = ∑ i ∈ range n, p ^ i := rfl

-- you don't need NeZero
lemma mu'_succ' {p n :ℕ} : mu' p (n+1) = p^n + mu' p n := by
  rw [mu'_def, mu'_def, sum_range_succ, add_comm]
  done

def mu (p:ℕ) : ℕ → ℕ
  | 0 => 0
  | n+1 => p * mu p n + 1

lemma mu_zero (p : ℕ) : mu p 0 = 0 := rfl

lemma mu_succ (p d : ℕ) : mu p (d + 1) = p * mu p d + 1 := rfl

example : mu = mu' := by
  ext p n
  unfold mu'
  induction n with
  | zero => rfl
  | succ d hd =>
    rw [mu_succ, hd, sum_range_succ', mul_sum]
    congr
    ext
    ring

Everything is easier with the Finset.sum definition because all the lemmas (in particular sum_range_succ and sum_range_succ') are already there so you don't have to reinvent the wheel.

[Ilmārs Cīrulis]

In case you still want proof of mu_succ' with your definition of mu.

import Mathlib

def mu (p:ℕ) : ℕ → ℕ
  | 0 => 0
  | n+1 => p * mu p n + 1

lemma mu_succ' {p n :ℕ} [NeZero p]: mu p (n+1) = p^n + mu p n := by
  induction n with
  | zero => simp [mu]
  | succ n iH => nth_rw 1 [mu, iH, mu]; ring

[Francisco Silva]

Thank you! This looks much simpler. I'll try to prove my other lemmas with this new definition.

[Kevin Buzzard]

The formula is more powerful than the recursive definition in this case because the only things the recursor gives you are the zero and succ lemmas, which are easily proved from the formula because we have a really solid API for Finset.sum. If the formula was super-hard to manipulate then there might be an argument for using the recursive definition, but not here.