OAI/GroupTheory/SimpleAmenable/PolygonGeometry/MatrixInverseCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.matrix_differentiableAt_det line 16
  2. theorem OAI.SimpleAmenable.matrix_differentiableAt_inverse line 21
  3. theorem OAI.SimpleAmenable.matrix_hasDerivAt_mul line 45
  4. theorem OAI.SimpleAmenable.matrix_hasDerivAt_inverse line 58
  5. theorem OAI.SimpleAmenable.matrix_hasDerivAt_mulVec line 82
  6. def OAI.SimpleAmenable.matrixAffineEquiv line 100
  7. theorem OAI.SimpleAmenable.matrixAffineEquiv_apply line 106
  8. theorem OAI.SimpleAmenable.matrixAffineEquiv_symm_apply line 112
  9. theorem OAI.SimpleAmenable.map_matrix_affine_volume line 120
  10. theorem OAI.SimpleAmenable.integral_matrix_affine line 129
  11. theorem OAI.SimpleAmenable.integral_matrix_affine_inverse line 139