NYLL
Module

Data.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Data
30 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Data

This module packages a finite quotient map with chosen section words. It defines the kernel, representatives, finite Schreier symbols, their evaluation, and the basic identities used by tau rewriting.

Imports1
Imported by2

Declarations

structure

FiniteQuotientSchreierData

L25 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData
Documentation

A finite quotient together with a normalized section.

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
Lean source · full declaration
structure FiniteQuotientSchreierData (X Q : Type*) [Group Q] [Fintype Q] where
  /-- The homomorphism from the free group to the finite quotient. -/
  quotientMap : FreeGroup X →* Q
  /-- A chosen free-group representative of each finite quotient element. -/
  quotientSection : Q → FreeGroup X
  /-- Each chosen representative maps back to the quotient element it represents. -/
  quotientMap_quotientSection : ∀ q, quotientMap (quotientSection q) = q
  /-- The identity quotient element is represented by the identity word. -/
  quotientSection_one : quotientSection 1 = 1
def

ofQuotientSectionWords

L41 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.ofQuotientSectionWords
Documentation

Finite quotient Schreier data can be built from quotient-section words whose evaluations are the prescribed quotient sections.

Source context 4 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
Lean source · full declaration
def ofQuotientSectionWords
    (quotientMap : FreeGroup X →* Q)
    (quotientSectionWord : Q → List (X × Bool))
    (quotientMap_mk_quotientSectionWord :
      ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q)
    (quotientSectionWord_one : quotientSectionWord 1 = []) :
    FiniteQuotientSchreierData X Q where
  quotientMap := quotientMap
  quotientSection q := FreeGroup.mk (quotientSectionWord q)
  quotientMap_quotientSection := quotientMap_mk_quotientSectionWord
  quotientSection_one := by
    simp only [quotientSectionWord_one, ← FreeGroup.one_eq_mk]
theorem

ofQuotientSectionWords_quotientSection

L59 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.ofQuotientSectionWords_quotientSection
Documentation

The finite quotient Schreier data built from quotient-section words has the prescribed quotient-section map.

Source context 4 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
Lean source · statement
theorem ofQuotientSectionWords_quotientSection
    (quotientMap : FreeGroup X →* Q)
    (quotientSectionWord : Q → List (X × Bool))
    (quotientMap_mk_quotientSectionWord :
      ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q)
    (quotientSectionWord_one : quotientSectionWord 1 = [])
    (q : Q) :
    (ofQuotientSectionWords quotientMap quotientSectionWord
      quotientMap_mk_quotientSectionWord quotientSectionWord_one).quotientSection q =
      FreeGroup.mk (quotientSectionWord q)
theorem

quotientMap_quotientSection_apply

L75 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientMap_quotientSection_apply
Documentation

Applying the quotient map to a chosen quotient section returns the original quotient element.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem quotientMap_quotientSection_apply (q : Q) :
    D.quotientMap (D.quotientSection q) = q
def

kernel

L80 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.kernel
Documentation

The kernel of the finite quotient map is the subgroup used in the finite Schreier data.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def kernel : Subgroup (FreeGroup X)
def

representative

L86 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.representative
Documentation

The representative map chooses the quotient section of the quotient class of a free-group word.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def representative (w : FreeGroup X) : FreeGroup X
theorem

representative_quotientSection

L91 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.representative_quotientSection
Documentation

The representative of a chosen quotient section is that quotient section.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem representative_quotientSection (q : Q) :
    D.representative (D.quotientSection q) = D.quotientSection q
theorem

representative_eq_quotientSection_quotientMap

L96 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.representative_eq_quotientSection_quotientMap
Documentation

The representative of a word is the quotient section of its quotient-map image.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem representative_eq_quotientSection_quotientMap (w : FreeGroup X) :
    D.representative w = D.quotientSection (D.quotientMap w)
theorem

representative_one

L101 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.representative_one
Documentation

The representative of the identity is the identity quotient section.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem representative_one : D.representative 1 = 1
def

rightSchreierRepresentative

L105 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.rightSchreierRepresentative
Documentation

A finite quotient section defines a right Schreier representative for the kernel subgroup.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · full declaration
def rightSchreierRepresentative :
    RightSchreierRepresentative D.kernel where
  representative := D.representative
  sameRightCoset := by
    intro g
    change D.quotientMap (g * (D.representative g)⁻¹) = 1
    simp only [representative, map_mul, map_inv, quotientMap_quotientSection_apply, mul_inv_cancel]
  representative_eq_of_sameRightCoset := by
    intro g h hgh
    have hgh' : D.quotientMap (g * h⁻¹) = 1 := by
      simpa [kernel] using hgh
    have hquot : D.quotientMap g = D.quotientMap h := by
      have hmap : D.quotientMap g * (D.quotientMap h)⁻¹ = 1 := by
        simpa using hgh'
      calc
        D.quotientMap g =
            D.quotientMap g * (D.quotientMap h)⁻¹ * D.quotientMap h := by
              group
        _ = D.quotientMap h := by
              rw [hmap]
              simp only [one_mul]
    simp only [representative, hquot]
  representative_one := D.representative_one
abbrev

FiniteSchreierSymbol

L130 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.FiniteSchreierSymbol
Documentation

Finite-indexed Schreier generator labels.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
abbrev FiniteSchreierSymbol (X Q : Type*)
def

transition

L136 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.transition
Documentation

The finite-quotient Schreier transition sends \(q\) and generator \(x\) to \(q\) multiplied by the quotient image of \(x\).

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def transition (q : Q) (x : X) : Q
def

inverseTransition

L143 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.inverseTransition
Documentation

The inverse finite-quotient Schreier transition sends \(q\) and generator \(x\) to \(q\) multiplied by the inverse of the quotient image of \(x\).

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def inverseTransition (q : Q) (x : X) : Q
theorem

transition_eq

L148 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.transition_eq
Documentation

The transition map is the one specified by the finite-quotient Schreier data.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem transition_eq (q : Q) (x : X) :
    D.transition q x = q * D.quotientMap (FreeGroup.of x)
theorem

inverseTransition_eq

L157 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.inverseTransition_eq
Documentation

The inverse transition multiplies the current quotient state by the inverse of the generator's quotient image.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem inverseTransition_eq (q : Q) (x : X) :
    D.inverseTransition q x = q * (D.quotientMap (FreeGroup.of x))⁻¹
def

schreierGenerator

L165 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.schreierGenerator
Documentation

The Schreier generator is the correction term \(t x \overline{t x}^{-1}\) attached to a representative and a generator.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def schreierGenerator (q : Q) (x : X) : FreeGroup X
def

symbolEval

L169 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval
Documentation

Evaluation of one finite Schreier symbol as its Schreier generator in the free group.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def symbolEval (z : FiniteSchreierSymbol X Q) : FreeGroup X
def

symbolEvalHom

L176 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom
Documentation

The homomorphism extending finite Schreier-symbol evaluation to the free group on Schreier symbols.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
def symbolEvalHom : FreeGroup (FiniteSchreierSymbol X Q) →* FreeGroup X
theorem

symbolEvalHom_of

L181 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom_of
Documentation

The evaluation homomorphism sends a Schreier-symbol generator to its symbol evaluation.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEvalHom_of (z : FiniteSchreierSymbol X Q) :
    D.symbolEvalHom (FreeGroup.of z) = D.symbolEval z
theorem

quotientMap_schreierGenerator_eq_one

L186 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientMap_schreierGenerator_eq_one
Documentation

The quotient map kills every finite Schreier generator.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem quotientMap_schreierGenerator_eq_one (q : Q) (x : X) :
    D.quotientMap (D.schreierGenerator q x) = 1
theorem

symbolEval_mem

L193 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval_mem
Documentation

Each evaluated finite Schreier symbol lies in the kernel of the quotient map.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEval_mem (z : FiniteSchreierSymbol X Q) :
    D.symbolEval z ∈ D.kernel
theorem

symbolEvalHom_mem

L202 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom_mem
Documentation

The image of the Schreier-symbol evaluation homomorphism lies in the kernel of the quotient map.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEvalHom_mem
    (q : FreeGroup (FiniteSchreierSymbol X Q)) :
    D.symbolEvalHom q ∈ D.kernel
def

symbolEvalSubgroupHom

L214 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalSubgroupHom
Documentation

Evaluation of Schreier symbols as a homomorphism into the kernel being rewritten.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · full declaration
def symbolEvalSubgroupHom :
    FreeGroup (FiniteSchreierSymbol X Q) →* D.kernel where
  toFun q := ⟨D.symbolEvalHom q, D.symbolEvalHom_mem q⟩
  map_one' := Subtype.ext D.symbolEvalHom.map_one
  map_mul' q r := Subtype.ext (D.symbolEvalHom.map_mul q r)
theorem

symbolEvalSubgroupHom_apply

L225 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalSubgroupHom_apply
Documentation

Forgetting the subgroup target of \(\mathrm{symbolEvalSubgroupHom}\) gives the ordinary evaluation homomorphism.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEvalSubgroupHom_apply
    (q : FreeGroup (FiniteSchreierSymbol X Q)) :
    (D.symbolEvalSubgroupHom q : FreeGroup X) = D.symbolEvalHom q
def

relatorSubgroup

L231 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.relatorSubgroup
Documentation

The subgroup of the kernel induced by the ambient normal closure of the original relators.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · full declaration
def relatorSubgroup
    (R : Set (FreeGroup X)) :
    Subgroup D.kernel where
  carrier := {g | (g : FreeGroup X) ∈ Subgroup.normalClosure R}
  one_mem' := by
    simp only [Set.mem_ofPred_eq, OneMemClass.coe_one, one_mem]
  mul_mem' := by
    intro a b ha hb
    exact Subgroup.mul_mem (Subgroup.normalClosure R) ha hb
  inv_mem' := by
    intro a ha
    exact Subgroup.inv_mem (Subgroup.normalClosure R) ha
instance

relatorSubgroup_normal

L245 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.relatorSubgroup_normal
Documentation

The subgroup generated by the relators of the presented group is normal.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · full declaration
instance relatorSubgroup_normal
    (R : Set (FreeGroup X)) :
    (D.relatorSubgroup R).Normal where
  conj_mem n hn g := by
    change ((g : FreeGroup X) * (n : FreeGroup X) * (g : FreeGroup X)⁻¹) ∈
      Subgroup.normalClosure R
    simpa [mul_assoc] using
      (Subgroup.normalClosure_normal.conj_mem
        (n : FreeGroup X) hn (g : FreeGroup X))
theorem

symbolEval_apply

L257 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval_apply
Documentation

Evaluation of a finite Schreier symbol is the corresponding Schreier generator formula.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEval_apply (q : Q) (x : X) :
    D.symbolEval (q, x) =
      D.quotientSection q * FreeGroup.of x *
        (D.quotientSection (D.transition q x))⁻¹
theorem

transition_after_inverseTransition

L267 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.transition_after_inverseTransition
Documentation

Applying the transition after the inverse transition for the same generator returns the original quotient element.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem transition_after_inverseTransition (q : Q) (x : X) :
    D.transition (D.inverseTransition q x) x = q
theorem

inverseTransition_after_transition

L277 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.inverseTransition_after_transition
Documentation

Applying the inverse transition after the transition for the same generator returns the original quotient element.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem inverseTransition_after_transition (q : Q) (x : X) :
    D.inverseTransition (D.transition q x) x = q
theorem

symbolEval_inverseTransition

L288 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval_inverseTransition
Documentation

Evaluation after an inverse transition has the expected representative formula ending at the original quotient class.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
Lean source · statement
theorem symbolEval_inverseTransition (q : Q) (x : X) :
    D.symbolEval (D.inverseTransition q x, x) =
      D.quotientSection (D.inverseTransition q x) *
        FreeGroup.of x * (D.quotientSection q)⁻¹

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.