OAI/NumberTheory/TotientAsymptotic/LocalOriginalDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-head errors vanish on the same fixed-prefix normalization as the positive candidate family.

  1. theorem OAI.TotientAsymptotic.ambient_residual_error_negligible line 14