OAI/Algebra/FiniteTensor/ComplementaryGraphs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Complementary graph matrices and tangent invertibility.

  1. def OAI.PD4Tensor.FiniteCoordinates.planeRestriction line 16
  2. theorem OAI.PD4Tensor.FiniteCoordinates.planeRestriction_coord line 20
  3. def OAI.PD4Tensor.FiniteCoordinates.combinedGraph line 29
  4. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_eval_left line 36
  5. def OAI.PD4Tensor.joinedMatrix line 60
  6. theorem OAI.PD4Tensor.joinedMatrix_mulVec line 63
  7. theorem OAI.PD4Tensor.joinedMatrix_det_ne_zero line 74
  8. theorem OAI.PD4Tensor.coeff_single_rename_embedding line 110
  9. theorem OAI.PD4Tensor.coeff_single_rename_outside line 116
  10. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_constantCoeff line 136
  11. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_coeff line 142
  12. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_central_tangent line 172