OAI/Geometry/RCD/Coordinates/MatrixTransverseDefect.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The same finite Gram defect controls the transverse derivative

  1. theorem OAI.RegularPointCoordinates.matrix_gram_row_defect line 12
  2. theorem OAI.RegularPointCoordinates.matrix_transverse_defect line 35