OAI/Combinatorics/HadwigerCounterexample/MatrixFactorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.invariant_cols line 15

   Source documentation

   Projecting the columns onto their literal column space keeps the matrix.

   theorem invariant_cols (M : Mat I J) (Z R) (e : colSp Z = colSp M)
       [DecidableEq Q] (hr : R*Z=(1:Mat Q Q)) :
       Z * (R*M) = M := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.colSp

2. theorem OAI.HadwigerCounterexample.rank_product line 28
3. theorem OAI.HadwigerCounterexample.rank_symmetric line 43

   Source documentation

   Symmetric nonsingular factor on the rank space.

   theorem rank_symmetric (M : Mat I I) (hm : Mᵀ=M) :
       ∃ (P : Mat I (Fin M.rank)) (G : Mat (Fin M.rank) (Fin M.rank)),
         Function.Injective P.mulVec ∧ Gᵀ=G ∧ Function.Injective G.mulVec ∧ P*G*Pᵀ=M := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat

4. theorem OAI.HadwigerCounterexample.matrix_cancel_left line 63
5. theorem OAI.HadwigerCounterexample.eigenbasis_idem line 70
6. theorem OAI.HadwigerCounterexample.diagonalize line 108