OAI/RingTheory/DirectFiniteness/ScalarWitnesses.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteBlock.matrixUnit line 14
2. lemma OAI.KaplanskyCounterexample.FiniteBlock.matrixUnit_diag line 18
3. lemma OAI.KaplanskyCounterexample.FiniteBlock.matrixUnit_mul line 22
4. lemma OAI.KaplanskyCounterexample.FiniteBlock.matrixUnit_ne_zero line 33
5. theorem OAI.KaplanskyCounterexample.FiniteBlock.scalar_witnesses line 40