OAI/NumberTheory/Jacobsthal/Sieve/FrozenSieveMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseFrozen.frozenIntegers line 14
  2. theorem OAI.Erdos970.ErdosInverseFrozen.frozenIntegers_card line 18
  3. theorem OAI.Erdos970.ErdosInverseFrozen.frozenIntegers_subset line 23
  4. theorem OAI.Erdos970.ErdosInverseFrozen.frozen_residueCount line 30
  5. def OAI.Erdos970.ErdosInverseFrozen.frozenExceptional line 39
  6. theorem OAI.Erdos970.ErdosInverseFrozen.mem_frozenExceptional line 43
  7. theorem OAI.Erdos970.ErdosInverseFrozen.frozen_upper line 60
  8. theorem OAI.Erdos970.ErdosInverseFrozen.frozen_exceptional_mean line 70