CellDifferenceGCD.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

GCD normalization of cell differences

Finite cell differences divided by their gcd generate every cyclic quotient. Reducing a set contained in [0,s] modulo s loses at most the upper endpoint.

theorem OAI.Ostmann.nat_gcd_mem_subgroup line 18
theorem OAI.Ostmann.finset_gcd_mem_subgroup line 28

theorem OAI.Ostmann.cyclic_closure_of_gcd_one line 39

Source documentation

A gcd-one set of nonnegative integers generates every cyclic quotient.

theorem cyclic_closure_of_gcd_one (A : Finset ℕ) (hA : A.gcd id = 1) (q : ℕ) :
    AddSubgroup.closure ((A.image (fun a : ℕ => (a : ZMod q)) : Finset (ZMod q)) : Set (ZMod q)) = ⊤ := by
…

theorem OAI.Ostmann.normalized_cyclic_closure line 54

Source documentation

GCD normalization gives the required generating set without a primitivity assumption on the original cell indices.

theorem normalized_cyclic_closure (A : Finset ℕ) (a : ℕ) (ha : a ∈ A) (ha0 : a ≠ 0)
    (q : ℕ) :
    AddSubgroup.closure
      ((A.image (fun b => b / A.gcd id)).image (fun b : ℕ => (b : ZMod q)) : Set (ZMod q)) = ⊤ := by
…

theorem OAI.Ostmann.card_residue_image_lower line 64

Source documentation

The only collision introduced on [0,s] by reduction modulo s is between the two endpoints.

theorem card_residue_image_lower (A : Finset ℕ) (s : ℕ) (_hs : 0 < s)
    (hbound : ∀ a ∈ A, a ≤ s) :
    A.card ≤ (A.image (fun a : ℕ => (a : ZMod s))).card + 1 := by
…