Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Schreier
ProCGroups/ReidemeisterSchreier/Schreier

ProCGroups.ReidemeisterSchreier.Schreier

6 Theorems | 1 Definition

This module formalizes Schreier generators and rewriting.

import
  • Mathlib.Data.Nat.Basic
Imported by

Declarations

Definition ReidemeisterSchreier.Schreier.rankTransform 
def rankTransform (r i : ℕ) : ℕ :=
  if r = 0 then 0 else 1 + i * (r - 1)

The Schreier rank transform \(T(r,i)=1+i(r-1)\), with the rank-zero convention.

Theorem ReidemeisterSchreier.Schreier.rankTransform_zero_left 
@[simp] theorem rankTransform_zero_left (i : ℕ) : rankTransform 0 i = 0

Schreier's rank transform satisfies the displayed cardinal-arithmetic identity.

Show Lean proof
Theorem ReidemeisterSchreier.Schreier.rankTransform_succ 
@[simp] theorem rankTransform_succ (r i : ℕ) : rankTransform (r + 1) i = 1 + i * r

Schreier's rank transform satisfies the displayed cardinal-arithmetic identity.

Show Lean proof
Theorem ReidemeisterSchreier.Schreier.rankTransform_one_left 
@[simp] theorem rankTransform_one_left (i : ℕ) : rankTransform 1 i = 1

Schreier's rank transform satisfies the displayed cardinal-arithmetic identity.

Show Lean proof
Theorem ReidemeisterSchreier.Schreier.rankTransform_eq_one_add 
theorem rankTransform_eq_one_add {r i : ℕ} (hr : r ≠ 0) :
    rankTransform r i = 1 + i * (r - 1)

For nonzero \(r\), the Schreier rank transform is \(1+i(r-1)\).

Show Lean proof
Theorem ReidemeisterSchreier.Schreier.rankTransform_mul_index 
theorem rankTransform_mul_index (r i j : ℕ) :
    rankTransform (rankTransform r i) j = rankTransform r (i * j)

Multiplying subgroup indices composes the Schreier rank transform.

Show Lean proof
Theorem ReidemeisterSchreier.Schreier.rankTransform_mono_left 
theorem rankTransform_mono_left {r s i : ℕ} (hrs : r ≤ s) :
    rankTransform r i ≤ rankTransform s i

The Schreier rank transform is monotone in the rank variable.

Show Lean proof