OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SumDvdDilateComplex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryAnalyticCentering.sum_dvd_dilate_complex line 28
2. def OAI.OrdinaryAnalyticCentering.choiceTerm line 53
3. lemma OAI.OrdinaryAnalyticCentering.centered_eq_raw_add line 59
4. lemma OAI.OrdinaryAnalyticCentering.choiceTerm_dilate line 99