OAI/RingTheory/DirectFiniteness/PrescribedData.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.Prescription.Output.h line 10
  2. abbrev OAI.KaplanskyCounterexample.Prescription.Output.q line 11
  3. abbrev OAI.KaplanskyCounterexample.Prescription.Output.ell line 12
  4. abbrev OAI.KaplanskyCounterexample.Prescription.Output.n line 13
  5. abbrev OAI.KaplanskyCounterexample.Prescription.Output.Coeff line 14
  6. abbrev OAI.KaplanskyCounterexample.Prescription.Output.Subfield line 15
  7. abbrev OAI.KaplanskyCounterexample.Prescription.Output.Ambient line 16
  8. abbrev OAI.KaplanskyCounterexample.Prescription.Output.holes line 17
  9. abbrev OAI.KaplanskyCounterexample.Prescription.Output.family line 18
  10. abbrev OAI.KaplanskyCounterexample.Prescription.Output.V line 19
  11. abbrev OAI.KaplanskyCounterexample.Prescription.Output.F line 20
  12. abbrev OAI.KaplanskyCounterexample.Prescription.Output.Slots line 21
  13. instance OAI.KaplanskyCounterexample.Prescription.Output.ell_prime line 23
  14. instance OAI.KaplanskyCounterexample.Prescription.Output.ambient_order line 25
  15. instance OAI.KaplanskyCounterexample.Prescription.Output.subsets_order line 26
  16. instance OAI.KaplanskyCounterexample.Prescription.Output.(instance at line 27) line 27
  17. instance OAI.KaplanskyCounterexample.Prescription.Output.(instance at line 28) line 28
  18. instance OAI.KaplanskyCounterexample.Prescription.Output.(instance at line 29) line 29
  19. instance OAI.KaplanskyCounterexample.Prescription.Output.(instance at line 30) line 30
  20. lemma OAI.KaplanskyCounterexample.Prescription.Output.success line 33
  21. def OAI.KaplanskyCounterexample.Prescription.Output.Inc line 35
  22. lemma OAI.KaplanskyCounterexample.Prescription.Output.mem_Inc line 36
  23. lemma OAI.KaplanskyCounterexample.Prescription.Output.nonempty_Inc line 38
  24. lemma OAI.KaplanskyCounterexample.Prescription.Output.degree_Inc line 41
  25. lemma OAI.KaplanskyCounterexample.Prescription.Output.girth_Inc line 46
  26. lemma OAI.KaplanskyCounterexample.Prescription.Output.ambient_card line 53
  27. lemma OAI.KaplanskyCounterexample.Prescription.Output.V_card line 56
  28. lemma OAI.KaplanskyCounterexample.Prescription.Output.sizes line 58
  29. def OAI.KaplanskyCounterexample.Prescription.Output.v0 line 66

    Source documentation

    The specified first point and first matrix coordinate in their inherited orders.

    def v0 : V := first (fun _ => True) (by
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.Output.V, OAI.KaplanskyCounterexample.Prescription.first

  30. def OAI.KaplanskyCounterexample.Prescription.Output.i0 line 69
  31. lemma OAI.KaplanskyCounterexample.Prescription.Output.v0_first line 72
  32. lemma OAI.KaplanskyCounterexample.Prescription.Output.i0_first line 73
  33. def OAI.KaplanskyCounterexample.Prescription.Output.assignment line 75
  34. def OAI.KaplanskyCounterexample.Prescription.Output.slot line 78
  35. def OAI.KaplanskyCounterexample.Prescription.Output.form line 79
  36. lemma OAI.KaplanskyCounterexample.Prescription.Output.forms_distinct line 81
  37. def OAI.KaplanskyCounterexample.Prescription.Output.X line 85

    Source documentation

    The unique interpolation columns over the actual prescribed root subfield.

    def X : Matrix Slots V Coeff := complementMatrix (enumeration h) holes

    Mentions: OAI.KaplanskyCounterexample.Prescription.Output.Slots, OAI.KaplanskyCounterexample.Prescription.Output.V, OAI.KaplanskyCounterexample.Prescription.Output.Coeff, OAI.KaplanskyCounterexample.Prescription.enumeration, OAI.KaplanskyCounterexample.Prescription.Output.h, OAI.KaplanskyCounterexample.Prescription.Output.holes

  38. lemma OAI.KaplanskyCounterexample.Prescription.Output.X_global line 86
  39. lemma OAI.KaplanskyCounterexample.Prescription.Output.X_local line 88