OAI/RingTheory/DirectFiniteness/PrescribedFields.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.Prescription.Input line 9
  2. def OAI.KaplanskyCounterexample.Prescription.fieldDegree line 11
  3. lemma OAI.KaplanskyCounterexample.Prescription.fieldDegree_pos line 12
  4. abbrev OAI.KaplanskyCounterexample.Prescription.K line 16
  5. instance OAI.KaplanskyCounterexample.Prescription.K_field line 17
  6. instance OAI.KaplanskyCounterexample.Prescription.K_char line 19
  7. abbrev OAI.KaplanskyCounterexample.Prescription.Q line 22
  8. instance OAI.KaplanskyCounterexample.Prescription.K_order line 24
  9. lemma OAI.KaplanskyCounterexample.Prescription.K_card line 26
  10. lemma OAI.KaplanskyCounterexample.Prescription.Q_card line 28
  11. def OAI.KaplanskyCounterexample.Prescription.enumeration line 34

    Source documentation

    The enumeration of the prescribed root subfield is in inherited coefficient order.

    def enumeration (h : Input) : Fin (Qcard h.val) ≃ Q h :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.Input, OAI.KaplanskyCounterexample.Prescription.Qcard, OAI.KaplanskyCounterexample.Prescription.Q

  12. lemma OAI.KaplanskyCounterexample.Prescription.primitive_exists line 37
  13. def OAI.KaplanskyCounterexample.Prescription.zeta line 49

    Source documentation

    The first element of multiplicative order ell in the literal coefficient order.

    def zeta (h : Input) : K h := first (fun ζ => IsPrimitiveRoot ζ (prime h.val)) (primitive_exists h)

    Mentions: OAI.KaplanskyCounterexample.Prescription.Input, OAI.KaplanskyCounterexample.Prescription.K, OAI.KaplanskyCounterexample.Prescription.first, OAI.KaplanskyCounterexample.Prescription.prime, OAI.KaplanskyCounterexample.Prescription.primitive_exists

  14. lemma OAI.KaplanskyCounterexample.Prescription.zeta_primitive line 50
  15. lemma OAI.KaplanskyCounterexample.Prescription.zeta_first line 53