OAI/Algebra/Determinantal/PunctualCharts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.CommutingPairs.nilpotent_pair_field_bound line 10
  2. theorem OAI.PermanentBorder.FieldParameters.adjoin_trdeg_le line 43
  3. theorem OAI.PermanentBorder.FieldParameters.field_adjoin_trdeg_le line 52
  4. theorem OAI.PermanentBorder.FieldParameters.extend_field line 58
  5. abbrev OAI.PermanentBorder.GenericMatrix.CoordinateRing line 85
  6. abbrev OAI.PermanentBorder.GenericMatrix.FunctionField line 86
  7. def OAI.PermanentBorder.GenericMatrix.coordinateMatrix line 87
  8. def OAI.PermanentBorder.GenericMatrix.genericMatrix line 89
  9. theorem OAI.PermanentBorder.GenericMatrix.coordinate_det_ne_zero line 92
  10. theorem OAI.PermanentBorder.GenericMatrix.generic_det_ne_zero line 102
  11. def OAI.PermanentBorder.GenericMatrix.genericUnit line 109
  12. theorem OAI.PermanentBorder.GenericMatrix.genericUnit_val line 112
  13. theorem OAI.PermanentBorder.GenericMatrix.relative_trdeg line 115
  14. theorem OAI.PermanentBorder.GenericMatrix.field_eq_top_of_mem line 125
  15. def OAI.PermanentBorder.CyclicFrames.MonomialBasis line 157
  16. theorem OAI.PermanentBorder.CyclicFrames.recover_frame line 160
  17. theorem OAI.PermanentBorder.CyclicFrames.pow_mem line 173
  18. theorem OAI.PermanentBorder.CyclicFrames.mulVec_mem line 185
  19. theorem OAI.PermanentBorder.CyclicFrames.frame_mem line 190
  20. theorem OAI.PermanentBorder.CyclicFrames.original_mem line 201
  21. theorem OAI.PermanentBorder.CyclicFrames.MonomialBasis.map line 229
  22. def OAI.PermanentBorder.CyclicFrames.conjugation line 247
  23. theorem OAI.PermanentBorder.CyclicFrames.conjugation_intertwines line 257
  24. def OAI.PermanentBorder.PunctualCharts.tripleEntries line 269
  25. theorem OAI.PermanentBorder.PunctualCharts.generated_chart_field_bound line 273
  26. theorem OAI.PermanentBorder.PunctualCharts.chart_field_bound line 338