OAI/Topology/ArtinGroups/Coxeter/RightParabolicDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.CoxeterExchange.exists_right_parabolic_decomposition line 9
2. lemma OAI.HarmonicArtin.CoxeterExchange.exists_right_descent line 22