OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteWordMetric.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete word metrics used in the metric-free main statement

  1. theorem OAI.PolycyclicRecognition.finite_lists_length_le line 14
  2. theorem OAI.PolycyclicRecognition.WordMetric.dist_eq line 31
  3. theorem OAI.PolycyclicRecognition.WordMetric.leftInvariant line 35
  4. theorem OAI.PolycyclicRecognition.WordMetric.discrete line 40
  5. theorem OAI.PolycyclicRecognition.WordMetric.finite_closedBall line 49
  6. theorem OAI.PolycyclicRecognition.WordMetric.proper line 63
  7. def OAI.PolycyclicRecognition.WordMetric.chains line 70

    Source documentation

    Prefixes of a shortest representing word form a unit-step chain whose length is the word distance.

    def chains : letI := P.normedGroup; LinearMetricChains G := by
…
  8. theorem OAI.PolycyclicRecognition.exists_finite_word_metric line 94

    Source documentation

    A finitely generated group admits the concrete proper, discrete word metric and its linear chains, without an external metric-existence input.

    theorem exists_finite_word_metric (G : Type*) [Group G] [Group.FG G] :
    ∃ d : MetricSpace G, letI := d
…