structure IncidenceGeometry.AffineLine (p : ℕ) [Fact (Nat.Prime p)] : Type

An affine line in (ℤ/p)^2, represented by coefficients (a, b, c) defining the equation a·x + b·y = c. The nondegeneracy condition a ≠ 0 ∨ b ≠ 0 ensures the equation truly cuts out a line.

• a : ZMod p
• b : ZMod p
• c : ZMod p
• nondegenerate : self.a ≠ 0 ∨ self.b ≠ 0

noncomputable def IncidenceGeometry.AffineLine.toFinset {p : ℕ} [hp : Fact (Nat.Prime p)] (L : AffineLine p) : Finset (ZMod p × ZMod p)

The set of points (x, y) ∈ (ℤ/p)^2 satisfying the line equation a·x + b·y = c, returned as a Finset.

def IncidenceGeometry.AffineLine.SamePointSet {p : ℕ} [hp : Fact (Nat.Prime p)] (L₁ L₂ : AffineLine p) : Prop

Two affine lines are considered equal when they have the same underlying point set in (ℤ/p)^2.

noncomputable def IncidenceGeometry.AffineLine.highFreq {p : ℕ} [hp : Fact (Nat.Prime p)] (L : AffineLine p) (x : ZMod p × ZMod p) : ℚ

The "high-frequency" component of the indicator of an affine line L at a point x: this is 1_L(x) - 1/p, i.e. the indicator with its mean (over the plane) subtracted. Used in the Fourier-analytic proof of the projection theorems.

theorem IncidenceGeometry.AffineLine.card_toFinset {p : ℕ} [hp : Fact (Nat.Prime p)] (L : AffineLine p) : L.toFinset.card = p

An affine line in (ℤ/p)^2 contains exactly p points.

theorem IncidenceGeometry.perp_transitivity {F : Type u_1} [Field F] {a₁ b₁ a₂ b₂ dx dy ux uy : F} (hnd1 : a₁ ≠ 0 ∨ b₁ ≠ 0) (hdir : dx ≠ 0 ∨ dy ≠ 0) (h1 : a₁ * dx + b₁ * dy = 0) (h2 : a₂ * dx + b₂ * dy = 0) (h3 : a₁ * ux + b₁ * uy = 0) : a₂ * ux + b₂ * uy = 0

Linear-algebraic transitivity lemma: if a nondegenerate normal (a₁, b₁) is perpendicular to both the direction (dx, dy) (also nondegenerate) and to a vector (ux, uy), and a second normal (a₂, b₂) is perpendicular to (dx, dy), then (a₂, b₂) is also perpendicular to (ux, uy). Used to show two distinct affine lines meet in at most one point.

theorem IncidenceGeometry.AffineLine.inter_card_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] (L₁ L₂ : AffineLine p) (h : ¬L₁.SamePointSet L₂) : (L₁.toFinset ∩ L₂.toFinset).card ≤ 1

Two distinct affine lines in (ℤ/p)^2 intersect in at most one point. (Here "distinct" is taken in the sense of ¬ SamePointSet.)