OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/AeNotNatTranslate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryInitialWidth.ae_not_nat_translate line 25
2. lemma OAI.OrdinaryInitialWidth.forward_eq_prefix line 36
3. lemma OAI.OrdinaryInitialWidth.forward_integral_le_prefix line 74