OAI/NumberTheory/TotientAsymptotic/Companion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The zero alternative for weighted totient counts when no arithmetic seed exists.

  1. lemma OAI.TotientAsymptotic.fk_nonneg line 13
  2. lemma OAI.TotientAsymptotic.fk_zero_of_le line 18
  3. lemma OAI.TotientAsymptotic.ell_le_mul_of_no_seed line 24
  4. lemma OAI.TotientAsymptotic.fk_ell_zero_of_no_seed line 30
  5. lemma OAI.TotientAsymptotic.N_zero_of_no_seed line 38
  6. lemma OAI.TotientAsymptotic.AH_zero_of_zero_weights line 56
  7. lemma OAI.TotientAsymptotic.AH_fk_zero_of_no_seed line 75
  8. lemma OAI.TotientAsymptotic.A_fk_zero_of_no_seed line 80
  9. theorem OAI.TotientAsymptotic.companion_zero_case line 87

    Distinct definitions of this name: ComparatorChallenges/TotientCompanionZero.lean:95 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.companion_zero_case@path.