OAI/RingTheory/DirectFiniteness/MatrixBlock.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.MatrixBlock.block line 13
2. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_zero line 15
3. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_add line 16
4. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_sub line 18
5. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_one line 20
6. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_mul line 27
7. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_sandwich line 54
8. lemma OAI.KaplanskyCounterexample.MatrixBlock.block_injective line 69
9. theorem OAI.KaplanskyCounterexample.MatrixBlock.scalar_witnesses line 81

   Source documentation

   A (possibly nonunital) injective matrix block carries one-sided inverses to one-sided inverses in the ambient ring using the complementary idempotent.

   theorem scalar_witnesses
       (hpure : ∀ x i j, f x * q i j = 0 → x = 0)
       (a b : Matrix m m S) (hab : a * b = 1) (hba : b * a ≠ 1) :
       ∃ a' b' : R, a' * b' = 1 ∧ b' * a' ≠ 1 := by
   …