OAI/NumberTheory/Ostmann/Construction/AtomTopSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The top atom support as explicit original-prime tests

  1. def OAI.Ostmann.atomPairChecks line 14

    Source documentation

    Every prime constituent of one atom is compared to every constituent of each different atom. Repeated coordinates are deliberately retained.

    noncomputable def atomPairChecks {I V : Type*} [Fintype I]
    (words : I → List V) : List (TopPrimeCondition V) :=
…

    Mentions: OAI.Ostmann.TopPrimeCondition

  2. theorem OAI.Ostmann.atomPairChecks_iff line 20
  3. theorem OAI.Ostmann.atomPairChecks_bounded line 53
  4. theorem OAI.Ostmann.atomPairChecks_length line 66
  5. def OAI.Ostmann.atomExternalChecks line 89
  6. theorem OAI.Ostmann.atomExternalChecks_iff line 93
  7. theorem OAI.Ostmann.atomExternalChecks_bounded line 109
  8. theorem OAI.Ostmann.atomExternalChecks_length line 117