ReidemeisterSchreier/Schreier.lean
1import Mathlib.Data.Nat.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Schreier.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Schreier rank transform
15-/
17namespace ReidemeisterSchreier
18namespace Schreier
20/-- The Schreier rank transform `T(r, i) = 1 + i * (r - 1)`, with the rank-zero convention. -/
21def rankTransform (r i : ℕ) : ℕ :=
22 if r = 0 then 0 else 1 + i * (r - 1)
24@[simp] theorem rankTransform_zero_left (i : ℕ) : rankTransform 0 i = 0 := by
25 simp only [rankTransform, ↓reduceIte]
27@[simp] theorem rankTransform_succ (r i : ℕ) : rankTransform (r + 1) i = 1 + i * r := by
28 simp only [rankTransform, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false, ↓reduceIte,
29 Nat.add_one_sub_one]
31@[simp] theorem rankTransform_one_left (i : ℕ) : rankTransform 1 i = 1 := by
32 simp only [rankTransform, Nat.succ_ne_self, ↓reduceIte, Nat.sub_self, Nat.mul_zero, Nat.add_zero]
34theorem rankTransform_eq_one_add {r i : ℕ} (hr : r ≠ 0) :
35 rankTransform r i = 1 + i * (r - 1) := by
36 simp only [rankTransform, hr, ↓reduceIte]
38/-- Multiplying subgroup indices composes the Schreier rank transform. -/
39theorem rankTransform_mul_index (r i j : ℕ) :
40 rankTransform (rankTransform r i) j = rankTransform r (i * j) := by
41 cases r with
43 simp only [rankTransform, ↓reduceIte]
44 | succ r =>
45 simp only [rankTransform, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false, ↓reduceIte,
46 Nat.add_one_sub_one, false_and, Nat.add_sub_cancel_left, Nat.mul_left_comm, Nat.mul_comm]
48/-- The Schreier rank transform is monotone in the rank variable. -/
49theorem rankTransform_mono_left {r s i : ℕ} (hrs : r ≤ s) :
50 rankTransform r i ≤ rankTransform s i := by
51 cases s with
53 have hr : r = 0 := Nat.eq_zero_of_le_zero hrs
54 subst hr
55 simp only [rankTransform_zero_left, le_refl]
56 | succ s =>
57 cases r with
59 simp only [rankTransform_zero_left, rankTransform_succ, Nat.zero_le]
60 | succ r =>
61 simpa only [rankTransform_succ] using
62 Nat.add_le_add_left (Nat.mul_le_mul_left i (Nat.succ_le_succ_iff.mp hrs)) 1
64end Schreier
65end ReidemeisterSchreier