OAI/RingTheory/DirectFiniteness/AlgebraicPacking.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.AlgebraicPacking.aMat line 13
2. def OAI.KaplanskyCounterexample.AlgebraicPacking.bMat line 16
3. theorem OAI.KaplanskyCounterexample.AlgebraicPacking.packing_identities line 19
4. theorem OAI.KaplanskyCounterexample.AlgebraicPacking.transpose_mul_ne_one line 70

   Source documentation

   The rank defect used after specialization to the subgroup algebra.

   theorem transpose_mul_ne_one {K : Type u_4} {m : Type u_5} {t : Type u_6} [Field K] [Fintype m] [Fintype t]
       (X : Matrix m t K) (hlt : Fintype.card m < Fintype.card t) :
       X.transpose * X ≠ 1 := by
   …

5. def OAI.KaplanskyCounterexample.AlgebraicPacking.Cpack line 78
6. def OAI.KaplanskyCounterexample.AlgebraicPacking.Jpack line 81
7. lemma OAI.KaplanskyCounterexample.AlgebraicPacking.Jpack_mul_Cpack line 85
8. theorem OAI.KaplanskyCounterexample.AlgebraicPacking.square_of_projections line 114