OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticLines.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.unitLineEquiv line 16

   Source documentation

   A feasible line on two unit coordinates has one point for each second coordinate.

   def unitLineEquiv {G : Type*} [CommGroup G] (a b : G) :
       {xy : G × G // a * xy.1 = b * xy.2} ≃ G where
   …

2. theorem OAI.Ostmann.card_unitLine line 29
3. def OAI.Ostmann.externalLineEquiv line 34

   Source documentation

   An external integer coordinate is unrestricted; the second coordinate is still a unit.

   noncomputable def externalLineEquiv {p : ℕ} [Fact p.Prime]
       (a : (ZMod p)ˣ) (b : ZMod p) :
       {xy : ZMod p × (ZMod p)ˣ // (a : ZMod p) * xy.1 = b * xy.2} ≃ (ZMod p)ˣ where
   …

4. theorem OAI.Ostmann.card_externalLine line 50
5. theorem OAI.Ostmann.unitLine_probability line 56
6. theorem OAI.Ostmann.externalLine_probability line 64
7. theorem OAI.Ostmann.independent_lines_no_unit_solution line 72
8. theorem OAI.Ostmann.line_zero_first_coefficient line 79
9. theorem OAI.Ostmann.dependent_lines_iff line 84

   Source documentation

   Vanishing two-by-two minors reduce all occurrence tests to one nonzero row.

   theorem dependent_lines_iff {K I : Type*} [Field K]
       (a b : I → K) (i : I) (ha : a i ≠ 0)
       (hdet : ∀ j, a i * b j - b i * a j = 0) (x y : K) :
       (∀ j, a j * x + b j * y = 0) ↔ a i * x + b i * y = 0 := by
   …