OAI/NumberTheory/TotientAsymptotic/SmoothTerminalEncoding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The small smooth terminal factors when only one prime survives.

  1. lemma OAI.TotientAsymptotic.smooth_terminal_factorization line 13
  2. lemma OAI.TotientAsymptotic.two_factorizations_card_le line 24
  3. lemma OAI.TotientAsymptotic.smooth_divisor_bound line 39
  4. abbrev OAI.TotientAsymptotic.SmoothTerminalTriple line 45
  5. def OAI.TotientAsymptotic.terminalFirst line 47
  6. def OAI.TotientAsymptotic.terminalMiddle line 49
  7. def OAI.TotientAsymptotic.terminalLast line 51
  8. def OAI.TotientAsymptotic.TerminalConditions line 54

    Source documentation

    The first coordinate is s; the equation is d*s=t*e.

    def TerminalConditions (d N : ℕ) (z : SmoothTerminalTriple) : Prop :=
…

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.SmoothTerminalTriple

  9. def OAI.TotientAsymptotic.terminalEncoding line 58
  10. lemma OAI.TotientAsymptotic.terminalEncoding_spec line 67