OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingAtomicProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Atomic intrinsic products give actual Dirac conditionals

  1. lemma OAI.DukePrimeDegree.pi_real_dirac_zero line 13
  2. theorem OAI.DukePrimeDegree.EliminationChain.remainingIntrinsicProduct_eq_dirac line 32
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.uncenteredIntrinsicProduct_eq_dirac line 60
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.intrinsicProductConditional_eq_dirac line 73
  5. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_conditionalKernel_eq_dirac_of_atomic_roots line 82