OAI/Topology/ArtinGroups/Geometry/Cartan.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.Geometric.cartan line 12
  2. lemma OAI.HarmonicArtin.Geometric.cartan_diag line 15
  3. lemma OAI.HarmonicArtin.Geometric.cartan_symm line 18
  4. def OAI.HarmonicArtin.Geometric.rootRow line 23
  5. lemma OAI.HarmonicArtin.Geometric.rootRow_apply line 26
  6. lemma OAI.HarmonicArtin.Geometric.rootRow_single line 29
  7. def OAI.HarmonicArtin.Geometric.simpleReflection line 33
  8. lemma OAI.HarmonicArtin.Geometric.simpleReflection_apply line 37
  9. lemma OAI.HarmonicArtin.Geometric.simpleReflection_squared line 40
  10. lemma OAI.HarmonicArtin.Geometric.simpleReflection_isLiftable line 46
  11. def OAI.HarmonicArtin.Geometric.representation line 60
  12. lemma OAI.HarmonicArtin.Geometric.representation_simple line 64
  13. lemma OAI.HarmonicArtin.Geometric.simple_injective line 67