OAI/GroupTheory/PolycyclicRecognition/Algebra/RealGramDeterminantOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of the positive Gram determinant

The concrete real-matrix form needed for expanding word-ball evaluations.

  1. theorem OAI.PolycyclicRecognition.real_matrix_eigenvalues_ge_one line 19
  2. theorem OAI.PolycyclicRecognition.real_matrix_det_ge_one line 33
  3. theorem OAI.PolycyclicRecognition.real_posDef_det_mono line 42
  4. theorem OAI.PolycyclicRecognition.real_posSemidef_det_mono line 71