OAI/NumberTheory/Ostmann/Construction/InitialTupleFrequencies.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The initial atom unit guard is precisely the Poisson frequency support

  1. theorem OAI.Ostmann.intCast_isUnit_iff_natAbs_coprime line 11
  2. theorem OAI.Ostmann.mem_tupleFrequencies_iff line 16