OAI/Topology/ArtinGroups/Coxeter/CommonWeakPrefixMaximal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.CoxeterExchange.common_weakPrefix_maximal_remove line 11
  2. theorem OAI.HarmonicArtin.CoxeterExchange.maximal_common_weakPrefix_greatest line 24
  3. theorem OAI.HarmonicArtin.CoxeterExchange.exists_greatest_common_weakPrefix line 78