This module formalizes Schreier generators and rewriting.
The Schreier rank transform \(T(r,i)=1+i(r-1)\), with the rank-zero convention.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreierdef rankTransform (r i : ℕ) : ℕSchreier's rank transform satisfies the displayed cardinal-arithmetic identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_zero_left (i : ℕ) : rankTransform 0 i = 0Schreier's rank transform satisfies the displayed cardinal-arithmetic identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_succ (r i : ℕ) : rankTransform (r + 1) i = 1 + i * rSchreier's rank transform satisfies the displayed cardinal-arithmetic identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_one_left (i : ℕ) : rankTransform 1 i = 1For nonzero \(r\), the Schreier rank transform is \(1+i(r-1)\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_eq_one_add {r i : ℕ} (hr : r ≠ 0) :
rankTransform r i = 1 + i * (r - 1)Multiplying subgroup indices composes the Schreier rank transform.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_mul_index (r i j : ℕ) :
rankTransform (rankTransform r i) j = rankTransform r (i * j)The Schreier rank transform is monotone in the rank variable.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
namespace Schreiertheorem rankTransform_mono_left {r s i : ℕ} (hrs : r ≤ s) :
rankTransform r i ≤ rankTransform s i