OAI/Geometry/PrescribedRicci/MatrixCofactorOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Matrix Cofactor Order.

  1. def OAI.MongeAmpere.cofactorQuadratic line 19
  2. lemma OAI.MongeAmpere.det_add_rankOne line 22
  3. lemma OAI.MongeAmpere.det_re_add_rankOne line 45
  4. lemma OAI.MongeAmpere.cofactorQuadratic_mono line 53
  5. lemma OAI.MongeAmpere.cofactorQuadratic_nonneg line 75
  6. lemma OAI.MongeAmpere.cofactorQuadratic_smul line 80
  7. lemma OAI.MongeAmpere.cofactorQuadratic_segment line 96