OAI/Algebra/OddKaplansky/MatrixUnits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.MatrixUnits.lift line 15
2. lemma OAI.OddKaplansky.MatrixUnits.lift_apply line 19
3. lemma OAI.OddKaplansky.MatrixUnits.lift_injective line 22
4. lemma OAI.OddKaplansky.MatrixUnits.lift_mul line 29
5. lemma OAI.OddKaplansky.MatrixUnits.regular_rank_bound line 44
6. lemma OAI.OddKaplansky.MatrixUnits.lift_idempotent line 74