OAI/Probability/SpanningForest/USTDeterminant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.FreeKernel.ustCylinder_positive_toReal_eq_det line 16
  2. theorem OAI.Problem336.FreeKernel.ustCylinder_positive_eq_det_of_contained line 42
  3. theorem OAI.Problem336.FreeKernel.ustCylinder_positive_eq_finiteKernel_det line 60