OAI/Geometry/PrescribedRicci/MatrixDifferentialNew.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Matrix Differential New.

  1. lemma OAI.MongeAmpere.contDiff_det line 15
  2. lemma OAI.MongeAmpere.differentiable_det line 24
  3. lemma OAI.MongeAmpere.fderiv_det_apply line 27
  4. lemma OAI.MongeAmpere.real_fderiv_det_apply line 40
  5. lemma OAI.MongeAmpere.contDiff_adjugate line 46
  6. lemma OAI.MongeAmpere.differentiableAt_inv line 64
  7. def OAI.MongeAmpere.matrixMulCLM line 70
  8. lemma OAI.MongeAmpere.real_fderiv_matrix_mul line 87
  9. lemma OAI.MongeAmpere.real_fderiv_inv_apply line 95
  10. lemma OAI.MongeAmpere.fderiv_inv_apply line 119
  11. lemma OAI.MongeAmpere.contDiffAt_inv line 125
  12. def OAI.MongeAmpere.weightedInverse line 130
  13. lemma OAI.MongeAmpere.contDiffAt_weightedInverse line 132
  14. lemma OAI.MongeAmpere.differentiableAt_weightedInverse line 136
  15. lemma OAI.MongeAmpere.fderiv_weightedInverse_apply line 140