OAI/Algebra/Determinantal/ConductorDuality.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.Conductor.algebraConductor line 11
  2. theorem OAI.PermanentBorder.Conductor.mem_algebraConductor line 24
  3. def OAI.PermanentBorder.Conductor.conductorMultiplication line 34
  4. theorem OAI.PermanentBorder.Conductor.conductorMultiplication_spec line 50
  5. theorem OAI.PermanentBorder.Conductor.conductorMultiplication_algebraMap line 54
  6. theorem OAI.PermanentBorder.Conductor.in_dual_restriction_image_iff line 72
  7. theorem OAI.PermanentBorder.Conductor.exists_dual_cokernel_equiv line 122
  8. theorem OAI.PermanentBorder.Conductor.dual_restriction_colength line 155
  9. def OAI.PermanentBorder.Conductor.topRemainderCoefficient line 171
  10. def OAI.PermanentBorder.Conductor.coefficientPairing line 174
  11. theorem OAI.PermanentBorder.Conductor.coefficientPairing_apply line 178
  12. theorem OAI.PermanentBorder.Conductor.topRemainderCoefficient_pow line 181
  13. def OAI.PermanentBorder.Conductor.pairingMatrix line 190
  14. theorem OAI.PermanentBorder.Conductor.pairingMatrix_apply line 195
  15. theorem OAI.PermanentBorder.Conductor.pairingMatrix_reverse_det line 205
  16. theorem OAI.PermanentBorder.Conductor.pairingMatrix_det_isUnit line 224
  17. def OAI.PermanentBorder.Conductor.coefficientPairingEquiv line 231
  18. theorem OAI.PermanentBorder.Conductor.coefficientPairingEquiv_apply line 238
  19. theorem OAI.PermanentBorder.Conductor.finrank_eq_of_denominators line 256
  20. theorem OAI.PermanentBorder.Conductor.conductor_colength line 274
  21. theorem OAI.PermanentBorder.Conductor.monic_conductor_colength line 310
  22. def OAI.PermanentBorder.Conductor.rootEvaluation line 333
  23. theorem OAI.PermanentBorder.Conductor.rootEvaluation_mk line 336
  24. theorem OAI.PermanentBorder.Conductor.rootEvaluation_injective line 342
  25. theorem OAI.PermanentBorder.Conductor.finite_integralClosure_adjoinRoot line 379