OAI/NumberTheory/Ostmann/Arithmetic/BulkRegularSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.pairwise_split_bulk line 12
2. theorem OAI.Ostmann.prime_list_pairwise_iff_nonbulk line 45

   Source documentation

   Under the original distinct-bulk event, all bulk coprimality tests are automatic. The nonbulk tests are retained exactly.

   theorem prime_list_pairwise_iff_nonbulk {σ : Type*} (value : σ → ℕ)
       (bulk : σ → Bool) (L : List σ)
       (hprime : ∀ i ∈ L, (value i).Prime)
       (hnodup : (L.filter bulk).Nodup)
       (hinj : ∀ i j, bulk i = true → bulk j = true → value i = value j → i = j)
       (hcross : ∀ i ∈ L, ∀ j ∈ L, bulk i ≠ bulk j → value i ≠ value j) :
       (L.map value).Pairwise Nat.Coprime ↔
         ((L.filter fun i => !(bulk i)).map value).Pairwise Nat.Coprime := by
   …