OAI/Topology/ArtinGroups/Geometry/ChamberCovector.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.Geometric.chamberCovector line 14
2. lemma OAI.HarmonicArtin.Geometric.chamberCovector_apply line 18
3. lemma OAI.HarmonicArtin.Geometric.chamberCovector_single line 21
4. lemma OAI.HarmonicArtin.Geometric.nonnegative_covector_root line 25
5. lemma OAI.HarmonicArtin.Geometric.orbit_dominant_bound line 31
6. lemma OAI.HarmonicArtin.Geometric.chamberCovector_parabolic_invariant line 55
7. theorem OAI.HarmonicArtin.Geometric.orbit_dominant_equality line 69
8. lemma OAI.HarmonicArtin.Geometric.orbitPoint_injective line 106