OAI/Algebra/Determinantal/PencilSeparability.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PermanentBorder.Conductor.charpoly_mem_adjugate_ideal line 11
2. def OAI.PermanentBorder.Conductor.polynomialCofactorQuotientEquiv line 18
3. theorem OAI.PermanentBorder.PencilSeparability.monic_generic_separable line 44
4. theorem OAI.PermanentBorder.PencilSeparability.separable_comp_linear line 70
5. theorem OAI.PermanentBorder.PencilSeparability.charpoly_smul_eq_comp line 90
6. theorem OAI.PermanentBorder.PencilSeparability.separable_charpoly_smul line 111
7. theorem OAI.PermanentBorder.PencilSeparability.distinct_slope_pencil_separable line 121
8. theorem OAI.PermanentBorder.AdjugateAlgebra.charmatrix_neg_eq_pencil line 169
9. theorem OAI.PermanentBorder.AdjugateAlgebra.cofactorIdeal_eq_matrixEntryIdeal line 176
10. theorem OAI.PermanentBorder.AdjugateAlgebra.critical_normalization_defect line 182