OAI/Algebra/Determinantal/Main.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PermanentBorder.SpectralPlane.slope line 10
2. def OAI.PermanentBorder.SpectralPlane.matrix line 12
3. def OAI.PermanentBorder.SpectralPlane.equation line 14
4. lemma OAI.PermanentBorder.SpectralPlane.scale_C line 17
5. lemma OAI.PermanentBorder.SpectralPlane.scale_linear line 22
6. lemma OAI.PermanentBorder.SpectralPlane.scale_matrix line 28
7. lemma OAI.PermanentBorder.SpectralPlane.totalDegree_equation line 47
8. lemma OAI.PermanentBorder.SpectralPlane.leading_equation line 55
9. lemma OAI.PermanentBorder.SpectralPlane.to_charpoly line 62
10. lemma OAI.PermanentBorder.SpectralPlane.homogeneous_leading line 80
11. lemma OAI.PermanentBorder.SpectralPlane.map_leading line 89
12. lemma OAI.PermanentBorder.SpectralDimension.curveField_le_of_inField line 103
13. lemma OAI.PermanentBorder.SpectralDimension.to_pencil_det line 118
14. theorem OAI.PermanentBorder.SpectralDimension.spectral_effective_bound line 131
15. lemma OAI.PermanentBorder.SpectralDimension.effective_matrix_budget line 205
16. theorem OAI.PermanentBorder.SpectralDimension.critical_dimension_effective line 214
17. def OAI.PermanentBorder.EffectiveParameters.sectionSize line 259
18. lemma OAI.PermanentBorder.EffectiveParameters.sectionSize_bounds line 261
19. lemma OAI.PermanentBorder.EffectiveParameters.degree_effective_bound line 298
20. theorem OAI.PermanentBorder.EffectiveParameters.explicit_constant line 313
21. theorem OAI.PermanentBorder.exists_effective_critical_bound line 344
22. theorem OAI.PermanentBorder.permanent_border_cubic_lower_bound line 364
23. theorem OAI.PermanentBorder.permanent_exact_cubic_lower_bound line 379
24. theorem OAI.PermanentBorder.permanent_cubic_lower_bounds line 384

    Distinct definitions of this name: ComparatorChallenges/PermanentCubic.lean:33 (same statement text; different proof or body). Qualify references as OAI.PermanentBorder.permanent_cubic_lower_bounds@path.