OAI/NumberTheory/TotientAsymptotic/OrderedPrimeProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact recovery of an ordered prime tuple from its product.

  1. lemma OAI.TotientAsymptotic.prime_coordinates_strictAnti line 11
  2. lemma OAI.TotientAsymptotic.ordered_prime_product_injective line 23