OAI/NumberTheory/JointDickman/Arithmetic/DivisorReindex.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.sum_divisors_reindex line 12

   Source documentation

   Reindex a divisibility condition by its quotient, retaining the exact finite endpoint and allowing the harmless zero term.

   theorem sum_divisors_reindex {M : Type*} [AddCommMonoid M]
       {a : ℕ} (ha : 0 < a) (N : ℕ) (F : ℕ → M) :
       (∑ n ∈ (range N).filter (fun n => a ∣ n), F n) =
         ∑ m ∈ (range N).filter (fun m => a*m < N), F (a*m) := by
   …

2. theorem OAI.JointDickman.sum_dvd_ite_reindex line 39

   Source documentation

   The same identity in indicator form, convenient inside coefficient sums.

   theorem sum_dvd_ite_reindex {M : Type*} [AddCommMonoid M]
       {a : ℕ} (ha : 0 < a) (N : ℕ) (F : ℕ → M) :
       (∑ n ∈ range N, if a ∣ n then F n else 0) =
         ∑ m ∈ range N, if a*m < N then F (a*m) else 0 := by
   …