OAI/Algebra/Determinantal/ConductorLocalization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.Conductor.normalization_conductor_le_adjugate line 15
  2. theorem OAI.PermanentBorder.Conductor.normalization_adjugate_length line 33
  3. def OAI.PermanentBorder.RootLocalization.changeRoot line 64
  4. theorem OAI.PermanentBorder.RootLocalization.changeRoot_mk line 67
  5. theorem OAI.PermanentBorder.RootLocalization.changeRoot_root line 73
  6. theorem OAI.PermanentBorder.RootLocalization.changeRoot_injective line 77
  7. theorem OAI.PermanentBorder.RootLocalization.changeRoot_denominators line 92
  8. theorem OAI.PermanentBorder.RootLocalization.changeRoot_isLocalizedModule line 100
  9. theorem OAI.PermanentBorder.ConductorLocalization.integral_conductor_localizes line 129
  10. def OAI.PermanentBorder.IdealLocalization.localizedIdeal line 152
  11. theorem OAI.PermanentBorder.IdealLocalization.map_le_localizedIdeal line 162
  12. theorem OAI.PermanentBorder.IdealLocalization.map_mem_localized line 168
  13. def OAI.PermanentBorder.Conductor.matrixRootChange line 181
  14. theorem OAI.PermanentBorder.Conductor.matrixRootChange_root line 185
  15. theorem OAI.PermanentBorder.Conductor.matrixRootChange_adjugate line 189
  16. theorem OAI.PermanentBorder.Conductor.matrixEntryIdeal_map line 219
  17. theorem OAI.PermanentBorder.Conductor.adjugateIdeal_baseChange line 227
  18. theorem OAI.PermanentBorder.Conductor.genericBaseChange_root line 241
  19. theorem OAI.PermanentBorder.Conductor.charpoly_map_tower line 252
  20. def OAI.PermanentBorder.Conductor.genericMatrixChange line 257
  21. theorem OAI.PermanentBorder.Conductor.genericMatrixChange_comp line 262
  22. theorem OAI.PermanentBorder.Conductor.integral_conductor_le_adjugate_local line 282
  23. theorem OAI.PermanentBorder.Conductor.normalization_conductor_le_adjugate_global line 304
  24. theorem OAI.PermanentBorder.Conductor.exists_conductor_cokernel_equiv line 356
  25. theorem OAI.PermanentBorder.Conductor.exists_normalization_conductor_cokernel_equiv line 393
  26. theorem OAI.PermanentBorder.Conductor.normalization_adjugate_length_global line 415