OAI/Topology/ArtinGroups/Geometry/Reflect.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.Geometric.reflect line 10
  2. lemma OAI.HarmonicArtin.Geometric.reflect_apply line 13
  3. lemma OAI.HarmonicArtin.Geometric.reflect_involutive line 16
  4. def OAI.HarmonicArtin.Geometric.reflection line 22
  5. lemma OAI.HarmonicArtin.Geometric.pair_left line 29
  6. lemma OAI.HarmonicArtin.Geometric.pair_right line 35
  7. lemma OAI.HarmonicArtin.Geometric.pair_difference line 41
  8. lemma OAI.HarmonicArtin.Geometric.pair_power_difference line 47
  9. def OAI.HarmonicArtin.Geometric.phase line 58
  10. lemma OAI.HarmonicArtin.Geometric.phase_quad line 60
  11. lemma OAI.HarmonicArtin.Geometric.phase_im line 64
  12. lemma OAI.HarmonicArtin.Geometric.pair_phase line 66
  13. lemma OAI.HarmonicArtin.Geometric.pair_phase_power line 79
  14. lemma OAI.HarmonicArtin.Geometric.phase_coordinates_injective line 92
  15. lemma OAI.HarmonicArtin.Geometric.pair_power_eq_id line 103