OAI/Topology/ArtinGroups/Geometry/CartanRestricted.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.Geometric.cartan_restricted line 17
  2. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_injective line 26
  3. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_add line 31
  4. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_sub line 35
  5. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_smul line 39
  6. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_single line 43
  7. lemma OAI.HarmonicArtin.Geometric.rootRow_extension line 53
  8. lemma OAI.HarmonicArtin.Geometric.reflection_extension line 63
  9. lemma OAI.HarmonicArtin.Geometric.representation_extension line 69
  10. theorem OAI.HarmonicArtin.Geometric.restrictionHom_injective line 79
  11. lemma OAI.HarmonicArtin.Geometric.coordinateExtension_nonneg_iff line 94
  12. theorem OAI.HarmonicArtin.Geometric.restriction_ascent_iff line 106