Module

Generators.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Generators

24 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Generators

From a right Schreier transversal, this module constructs canonical representatives and Schreier generators, identifies the nontrivial representative-generator pairs, and proves their basic action identities.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

Imported by2

def

schreierTransversalRightCosetAction

L30 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierTransversalRightCosetAction

Documentation

The Schreier transversal itself carries the same right-coset action, transported along the equivalence with right cosets.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

def schreierTransversalRightCosetAction
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    MulAction (FreeGroup X) T

def

schreierRepresentative

L49 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative

Documentation

The chosen representative of a right coset attached to a right Schreier transversal.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

def schreierRepresentative {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    FreeGroup X → T

theorem

schreierRepresentative_eq_of_mem

L56 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative_eq_of_mem

Documentation

An element of the Schreier transversal is its own chosen representative.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierRepresentative_eq_of_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
  schreierRepresentative (X := X) hT t = ⟨t, ht⟩

theorem

schreierRepresentative_eq_one_of_mem

L66 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative_eq_one_of_mem

Documentation

Every element of the subgroup has the identity as its chosen Schreier representative.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierRepresentative_eq_one_of_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {g : FreeGroup X} (hg : g ∈ L) :
    schreierRepresentative (X := X) hT g = ⟨1, hT.2.1⟩

theorem

schreierRepresentative_eq_of_mem_mul_inv_mem

L79 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative_eq_of_mem_mul_inv_mem

Documentation

If \(t\) lies in the transversal and \(g t^{-1}\) lies in the subgroup, then \(t\) is the chosen representative of \(g\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierRepresentative_eq_of_mem_mul_inv_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {g t : FreeGroup X} (ht : t ∈ T) (hgt : g * t⁻¹ ∈ L) :
    schreierRepresentative (X := X) hT g = ⟨t, ht⟩

theorem

prefixParent_mem_of_mem

L89 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.prefixParent_mem_of_mem

Documentation

Membership of a word in the prefix tree implies membership of its prefix parent.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem prefixParent_mem_of_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    FreeGroup.prefixParent t ∈ T

theorem

schreierTransversalRightCosetAction_smul

L102 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierTransversalRightCosetAction_smul

Documentation

The right-coset action updates a Schreier representative by multiplying on the right and then choosing the representative of the resulting coset.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · full declaration

theorem schreierTransversalRightCosetAction_smul {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (g : FreeGroup X) (t : T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    g • t = schreierRepresentative (X := X) hT ((t : FreeGroup X) * g⁻¹) := by
  let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm
  have ht : e t = Quotient.mk'' (t : FreeGroup X) := by
    simpa [e] using (hT.1.mk''_rightQuotientEquiv (e t)).symm
  change
      hT.1.rightQuotientEquiv (g • hT.1.rightQuotientEquiv.symm t) =
        hT.1.rightQuotientEquiv (Quotient.mk'' ((t : FreeGroup X) * g⁻¹))
  rw [ht, rightCosetLeftMulActionByInverse_mk_smul]

def

schreierGenerator

L117 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator

Documentation

The Schreier expression attached to any word \(t\) and basis element \(x\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

def schreierGenerator {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) (t : FreeGroup X) (x : X) : L

abbrev

NontrivialSchreierPair

L130 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.NontrivialSchreierPair

Documentation

The canonical index type for the nontrivial Schreier generators attached to a right Schreier transversal. This pair-indexed type is the preferred basis index; the value-set Schreier generator set records the same nontrivial generators by their subgroup values.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

abbrev NontrivialSchreierPair {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) : Type u

def

nontrivialSchreierPairGenerator

L136 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.nontrivialSchreierPairGenerator

Documentation

The Schreier generator value represented by a nontrivial Schreier pair.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

def nontrivialSchreierPairGenerator {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    NontrivialSchreierPair (X := X) hT → L

theorem

nontrivialSchreierPairGenerator_apply

L145 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.nontrivialSchreierPairGenerator_apply

Documentation

The Schreier generator or pair map is evaluated by the chosen section and coset representative.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem nontrivialSchreierPairGenerator_apply {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (p : NontrivialSchreierPair (X := X) hT) :
    nontrivialSchreierPairGenerator (X := X) hT p =
      schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2

def

schreierGeneratorSet

L158 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorSet

Documentation

The classical Schreier generator value set attached to a right Schreier transversal. This value set records the resulting Schreier generators, while the nontrivial Schreier pairs provide the preferred basis index.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

def schreierGeneratorSet {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) : Set L

theorem

mem_schreierGeneratorSet_iff

L164 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.mem_schreierGeneratorSet_iff

Documentation

Membership in the Schreier generator set is equivalent to the displayed generator condition.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem mem_schreierGeneratorSet_iff {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    {hT : IsRightSchreierTransversal (X := X) L T} {z : L} :
    z ∈ schreierGeneratorSet (X := X) hT ↔
      ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1

theorem

schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one

L175 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one

Documentation

A nontrivial Schreier generator associated to an element of the transversal lies in the Schreier generator set.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) (x : X)
    (hne : schreierGenerator (X := X) hT t x ≠ 1) :
    schreierGenerator (X := X) hT t x ∈ schreierGeneratorSet (X := X) hT

theorem

schreierGenerator_mem_schreierGeneratorSet_of_ne_one

L185 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_mem_schreierGeneratorSet_of_ne_one

Documentation

A nontrivial Schreier generator belongs to the Schreier generator set.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_mem_schreierGeneratorSet_of_ne_one
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) (x : X)
    (hne : schreierGenerator (X := X) hT (t : FreeGroup X) x ≠ 1) :
    schreierGenerator (X := X) hT (t : FreeGroup X) x ∈
      schreierGeneratorSet (X := X) hT

theorem

schreierGeneratorSet_eq_range_nontrivialSchreierPairGenerator

L197 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorSet_eq_range_nontrivialSchreierPairGenerator

Documentation

The value-set formulation is precisely the range of the pair-indexed generator map.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGeneratorSet_eq_range_nontrivialSchreierPairGenerator
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    schreierGeneratorSet (X := X) hT =
      Set.range (nontrivialSchreierPairGenerator (X := X) hT)

theorem

schreierGenerator_eq_one_of_mem

L215 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_of_mem

Documentation

The Schreier generator is trivial exactly in the corresponding subgroup-membership case.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_eq_one_of_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} {x : X}
    (htx : t * FreeGroup.of x ∈ T) :
    schreierGenerator (X := X) hT t x = 1

theorem

schreierGenerator_eq_of_mul_mem

L230 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_of_mul_mem

Documentation

If the representative-generator product lies in the subgroup, the corresponding Schreier generator is the represented subgroup element.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_eq_of_mul_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} {x : X}
    (htx : t * FreeGroup.of x ∈ L) :
    schreierGenerator (X := X) hT t x = ⟨t * FreeGroup.of x, htx⟩

theorem

schreierGenerator_eq_one_iff

L241 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_iff

Documentation

The Schreier generator is trivial exactly under the corresponding coset condition.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_eq_one_iff {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    {hT : IsRightSchreierTransversal (X := X) L T}
    {t : FreeGroup X} {x : X} :
    schreierGenerator (X := X) hT t x = 1 ↔
      ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X) =
        t * FreeGroup.of x

theorem

exists_rightSchreierTransversal_of_minimalGeneratorPower

L268 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.exists_rightSchreierTransversal_of_minimalGeneratorPower

Documentation

Pointed discrete Reidemeister--Schreier statement: if \(x^N\) is the first positive power of a free generator landing in \(L\), one may choose a right Schreier transversal whose distinguished Schreier generator is exactly \(x^N\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem exists_rightSchreierTransversal_of_minimalGeneratorPower
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : (FreeGroup.of x) ^ N ∈ L)
    (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
    ∃ T : Set (FreeGroup X), ∃ hT : IsRightSchreierTransversal (X := X) L T,
      (FreeGroup.of x) ^ (N - 1) ∈ T ∧
        schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
          ⟨(FreeGroup.of x) ^ N, hpow⟩

theorem

schreierRepresentative_eq_prefixParent_of_cancels

L309 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative_eq_prefixParent_of_cancels

Documentation

If the last letter of a transversal word cancels with x, the Schreier representative of t x is the prefix parent of t.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierRepresentative_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} {x : X}
    (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
    (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
    schreierRepresentative (X := X) hT (t * FreeGroup.of x) =
      ⟨FreeGroup.prefixParent t, prefixParent_mem_of_mem (X := X) hT ht⟩

theorem

schreierRepresentative_eq_of_prefixParent_last_pos

L324 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRepresentative_eq_of_prefixParent_last_pos

Documentation

If a transversal word ends in x, the Schreier representative of its prefix parent multiplied by x is the original word.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierRepresentative_eq_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) {x : X}
    (hw : FreeGroup.toWord t ≠ [])
    (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
    schreierRepresentative (X := X) hT (FreeGroup.prefixParent t * FreeGroup.of x) = ⟨t, ht⟩

theorem

schreierGenerator_eq_one_of_cancels

L338 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_of_cancels

Documentation

If the last letter of a transversal word cancels with x, the corresponding Schreier generator is trivial.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_eq_one_of_cancels {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} {x : X}
    (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
    (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
    schreierGenerator (X := X) hT t x = 1

theorem

schreierGenerator_eq_one_of_prefixParent_last_pos

L353 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_of_prefixParent_last_pos

Documentation

If a transversal word ends in x, the Schreier generator attached to its prefix parent and x is trivial.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierGenerators
open scoped Pointwise
open _root_.ReidemeisterSchreier.FreeGroup

Lean source · statement

theorem schreierGenerator_eq_one_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) {x : X}
    (hw : FreeGroup.toWord t ≠ [])
    (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
    schreierGenerator (X := X) hT (FreeGroup.prefixParent t) x = 1

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Generators

Declarations