OAI/Geometry/EinsteinFour/PositiveDeterminantOrder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Determinant monotonicity for the positive matrices in radial comparison.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.one_le_det_one_add_posSemidef line 12
  2. theorem OAI.PositiveEinsteinFour.Jacobi.det_le_det_of_posDef_sub_posSemidef line 34