OAI/Algebra/Determinantal/Normalization.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.Conductor.genericBaseChange line 12
  2. theorem OAI.PermanentBorder.Conductor.genericBaseChange_mk line 17
  3. theorem OAI.PermanentBorder.Conductor.genericBaseChange_injective line 25
  4. theorem OAI.PermanentBorder.Conductor.genericBaseChange_denominators line 36
  5. def OAI.PermanentBorder.Conductor.normalizationInclusion line 49
  6. theorem OAI.PermanentBorder.Conductor.normalizationInclusion_val line 56
  7. theorem OAI.PermanentBorder.Conductor.normalizationInclusion_injective line 60
  8. theorem OAI.PermanentBorder.Conductor.normalizationInclusion_denominators line 66
  9. theorem OAI.PermanentBorder.Conductor.normalization_torsionFree line 85
  10. theorem OAI.PermanentBorder.Conductor.normalization_conductor_colength line 98
  11. theorem OAI.PermanentBorder.Conductor.exists_splitting_eigenbasis line 121
  12. theorem OAI.PermanentBorder.Conductor.exists_ground_vector_all_coords_ne_zero line 148
  13. theorem OAI.PermanentBorder.Conductor.eigenbasis_coord_apply line 183
  14. theorem OAI.PermanentBorder.Conductor.eigenbasis_coord_pow line 197
  15. theorem OAI.PermanentBorder.Conductor.eigenbasis_coord_aeval line 206
  16. theorem OAI.PermanentBorder.Conductor.matrix_aeval_mulVec line 219
  17. theorem OAI.PermanentBorder.Conductor.matrix_aeval_map_mulVec line 225
  18. def OAI.PermanentBorder.Conductor.cyclicMap line 250
  19. theorem OAI.PermanentBorder.Conductor.cyclicMap_mk line 264
  20. theorem OAI.PermanentBorder.Conductor.cyclicMap_root_mul line 267
  21. theorem OAI.PermanentBorder.Conductor.exists_cyclicMap_bijective line 282
  22. theorem OAI.PermanentBorder.Conductor.exists_generic_matrix_equiv line 315
  23. theorem OAI.PermanentBorder.Conductor.finite_maximalSpectrum_of_finite_local line 337
  24. theorem OAI.PermanentBorder.Conductor.integralClosure_isPrincipalIdealRing line 381