OAI/RingTheory/DirectFiniteness/LexicographicOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Prescription.first line 12

   Source documentation

   First successful element of a finite, linearly ordered search space.

   def first {α : Type u_1} [Fintype α] [LinearOrder α] (P : α → Prop) (h : ∃ x, P x) : α :=
   …

2. lemma OAI.KaplanskyCounterexample.Prescription.first_spec line 15
3. lemma OAI.KaplanskyCounterexample.Prescription.first_le line 20
4. def OAI.KaplanskyCounterexample.Prescription.vectorOrder line 25

   Source documentation

   Lexicographic order on coefficient/coordinate vectors, increasing index first.

   @[instance_reducible] def vectorOrder {ι : Type u_4} [LinearOrder ι] [WellFoundedLT ι]
       {α : Type u_5} [LinearOrder α] : LinearOrder (ι → α) :=
   …

5. def OAI.KaplanskyCounterexample.Prescription.subsetOrder line 29
6. def OAI.KaplanskyCounterexample.Prescription.residueOrder line 39

   Source documentation

   Residues are ordered 0,...,p-1, independently of their field operations.

   @[instance_reducible] def residueOrder (p : ℕ) [NeZero p] : LinearOrder (ZMod p) :=
   …