OAI/Algebra/OddKaplansky/AugmentInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.LocalAlgebra.scalarMatrix line 17
2. def OAI.OddKaplansky.LocalAlgebra.scalarInverse line 20
3. lemma OAI.OddKaplansky.LocalAlgebra.scalar_map line 22
4. lemma OAI.OddKaplansky.LocalAlgebra.scalar_products line 34
5. lemma OAI.OddKaplansky.LocalAlgebra.error_entry_mem line 48
6. lemma OAI.OddKaplansky.LocalAlgebra.error_nil line 55
7. lemma OAI.OddKaplansky.LocalAlgebra.matrix_inverse_formula line 64