OAI/Algebra/Determinantal/CurveParameters.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.CurveParameters.support_field_bound line 11
  2. theorem OAI.PermanentBorder.CurveParameters.extend_by_chart line 19
  3. structure OAI.PermanentBorder.CurveParameters.LocalChart line 75
  4. def OAI.PermanentBorder.CurveParameters.LocalChart.InField line 93
  5. theorem OAI.PermanentBorder.CurveParameters.LocalChart.InField.mono line 97
  6. theorem OAI.PermanentBorder.CurveParameters.LocalChart.extend line 102
  7. theorem OAI.PermanentBorder.CurveParameters.extend_by_finite_family line 111
  8. theorem OAI.PermanentBorder.FiniteAlgebras.artinian line 141
  9. theorem OAI.PermanentBorder.FiniteAlgebras.exists_local_power_decomposition line 143
  10. theorem OAI.PermanentBorder.FiniteAlgebras.maximal_power_ne_top line 154
  11. theorem OAI.PermanentBorder.FiniteAlgebras.scalar_residue line 159
  12. theorem OAI.PermanentBorder.FiniteAlgebras.translated_coordinate_nilpotent line 169
  13. theorem OAI.PermanentBorder.FiniteAlgebras.finrank_sum_of_equiv line 179
  14. def OAI.PermanentBorder.FiniteAlgebras.residueEquiv line 194
  15. def OAI.PermanentBorder.FiniteAlgebras.residue line 201
  16. theorem OAI.PermanentBorder.FiniteAlgebras.sub_residue_mem line 204
  17. theorem OAI.PermanentBorder.FiniteAlgebras.residue_nilpotent line 212
  18. def OAI.PermanentBorder.FiniteAlgebras.supportPoint line 221
  19. theorem OAI.PermanentBorder.FiniteAlgebras.supportPoint_on_curve line 224
  20. def OAI.PermanentBorder.PlaneTranslations.translate line 238
  21. theorem OAI.PermanentBorder.PlaneTranslations.translate_X line 242
  22. theorem OAI.PermanentBorder.PlaneTranslations.translate_C line 245
  23. theorem OAI.PermanentBorder.PlaneTranslations.translate_comp line 248
  24. def OAI.PermanentBorder.PlaneTranslations.equivalence line 254
  25. theorem OAI.PermanentBorder.PlaneTranslations.equivalence_X line 260
  26. def OAI.PermanentBorder.FinitePlaneFrames.representation line 270
  27. def OAI.PermanentBorder.FinitePlaneFrames.unitVector line 274
  28. theorem OAI.PermanentBorder.FinitePlaneFrames.action_on_unit line 276
  29. theorem OAI.PermanentBorder.FinitePlaneFrames.exists_monomial_basis line 285
  30. def OAI.PermanentBorder.FiniteAlgebras.localHom line 322
  31. def OAI.PermanentBorder.FiniteAlgebras.shiftedLocalHom line 327
  32. theorem OAI.PermanentBorder.FiniteAlgebras.shiftedLocalHom_X line 332
  33. theorem OAI.PermanentBorder.FiniteAlgebras.shiftedLocalHom_surjective line 343
  34. theorem OAI.PermanentBorder.FiniteAlgebras.shiftedLocalHom_X_nilpotent line 349
  35. theorem OAI.PermanentBorder.FiniteAlgebras.local_length_pos line 357
  36. theorem OAI.PermanentBorder.FiniteAlgebras.local_monomial_chart line 363
  37. theorem OAI.PermanentBorder.FiniteAlgebras.exists_canonical_local_power_decomposition line 387
  38. theorem OAI.PermanentBorder.BasisFieldRecovery.repr_mem line 406
  39. theorem OAI.PermanentBorder.MatrixSubfield.pow_mem line 435
  40. theorem OAI.PermanentBorder.MatrixSubfield.mulVec_mem line 442