OAI/Algebra/Determinantal/QuotientFields.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.FinitePlaneFrames.monomial_coordinates_mem line 9
  2. theorem OAI.PermanentBorder.FinitePlaneFrames.unshifted_representation_mem line 24
  3. def OAI.PermanentBorder.FiniteAlgebras.localChart line 46
  4. theorem OAI.PermanentBorder.FiniteAlgebras.local_monomial_coordinates_mem line 74
  5. theorem OAI.PermanentBorder.CurveQuotientParameters.chart_field_bound line 100
  6. theorem OAI.PermanentBorder.AdjugateAlgebra.planeMap_single line 171
  7. def OAI.PermanentBorder.AdjugateAlgebra.rowCoordinateMap line 182
  8. theorem OAI.PermanentBorder.AdjugateAlgebra.rowCoordinateMap_bijective line 187
  9. def OAI.PermanentBorder.AdjugateAlgebra.rowCoordinates line 210
  10. def OAI.PermanentBorder.AdjugateAlgebra.rowBasis line 215
  11. theorem OAI.PermanentBorder.AdjugateAlgebra.rowBasis_apply line 220
  12. theorem OAI.PermanentBorder.AdjugateAlgebra.rowBasis_repr line 229
  13. def OAI.PermanentBorder.Bivariate.equivalence line 255
  14. theorem OAI.PermanentBorder.Bivariate.equivalence_X_zero line 259
  15. theorem OAI.PermanentBorder.Bivariate.equivalence_X_one line 263
  16. theorem OAI.PermanentBorder.Bivariate.equivalence_C line 270
  17. def OAI.PermanentBorder.Bivariate.map line 275
  18. theorem OAI.PermanentBorder.Bivariate.equivalence_map line 278
  19. theorem OAI.PermanentBorder.Bivariate.equivalence_monomial line 289
  20. def OAI.PermanentBorder.Bivariate.InField line 303
  21. theorem OAI.PermanentBorder.Bivariate.inField_iff_lifts line 306
  22. theorem OAI.PermanentBorder.Bivariate.InField.add line 325
  23. theorem OAI.PermanentBorder.Bivariate.InField.sub line 331
  24. theorem OAI.PermanentBorder.Bivariate.InField.mul line 337
  25. theorem OAI.PermanentBorder.Bivariate.inField_map line 343
  26. theorem OAI.PermanentBorder.Bivariate.inField_C_C line 349
  27. theorem OAI.PermanentBorder.Bivariate.inField_X line 354
  28. theorem OAI.PermanentBorder.Bivariate.inField_C_X line 357
  29. theorem OAI.PermanentBorder.Bivariate.eval_mem line 360
  30. theorem OAI.PermanentBorder.AdjugateAlgebra.coordinates_mem line 371
  31. theorem OAI.PermanentBorder.AdjugateAlgebra.scaled_coeff_mem line 390
  32. theorem OAI.PermanentBorder.AdjugateAlgebra.map_rowEntry line 400