OAI/Algebra/Determinantal/ConductorBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.Conductor.principal_coordinate line 10
  2. theorem OAI.PermanentBorder.Conductor.simultaneous_unit_combination line 59
  3. theorem OAI.PermanentBorder.Conductor.simultaneous_coordinate_generator line 94
  4. theorem OAI.PermanentBorder.Conductor.isIntegral_of_coordinates line 132
  5. theorem OAI.PermanentBorder.Conductor.isUnit_of_coordinates line 148
  6. theorem OAI.PermanentBorder.Conductor.exists_normalizing_lattice_element line 176
  7. theorem OAI.PermanentBorder.Conductor.exists_normalizing_matrix_generators line 238
  8. abbrev OAI.PermanentBorder.Conductor.DetQuotient line 307
  9. theorem OAI.PermanentBorder.Conductor.kernel_eq_adjugate_image line 309
  10. theorem OAI.PermanentBorder.Conductor.row_kernel_eq_adjugate_image line 354
  11. def OAI.PermanentBorder.Conductor.matrixEntryIdeal line 374
  12. theorem OAI.PermanentBorder.Conductor.entry_mem_matrixEntryIdeal line 378
  13. theorem OAI.PermanentBorder.Conductor.mapped_charmatrix line 383
  14. theorem OAI.PermanentBorder.Conductor.conductor_mem_adjugate_of_lattice line 392