OAI/Algebra/OddKaplansky/WeightedProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.WeightedProjection.gram line 14
2. def OAI.OddKaplansky.WeightedProjection.projection line 15
3. lemma OAI.OddKaplansky.WeightedProjection.fixes line 17
4. lemma OAI.OddKaplansky.WeightedProjection.idempotent line 21
5. lemma OAI.OddKaplansky.WeightedProjection.rank line 27
6. lemma OAI.OddKaplansky.WeightedProjection.annihilate_left line 35
7. lemma OAI.OddKaplansky.WeightedProjection.annihilate_right line 39
8. lemma OAI.OddKaplansky.WeightedProjection.conjugate_sub_pow line 45
9. lemma OAI.OddKaplansky.WeightedProjection.conjugate_annihilate line 57