OAI/Computability/PerfectCompleteness/Algebra/MatrixInverseConstantsLemmas.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.MatrixInverseConstants.exists_cutoff_density line 13
2. theorem OAI.PerfectCompleteness.LowerRankParameters.power_ratio_le line 45
3. theorem OAI.PerfectCompleteness.LowerRankParameters.exists_cross_parameters line 52
4. theorem OAI.PerfectCompleteness.LowerRankParameters.exists_lower_parameters line 68