OAI/NumberTheory/Ostmann/Arithmetic/PrimeCellJointReplacementPrior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PrimeCellReplacement.jointUnitTest line 14
2. lemma OAI.Ostmann.Arithmetic.PrimeCellReplacement.jointUnitTest_units line 19
3. lemma OAI.Ostmann.Arithmetic.PrimeCellReplacement.jointUnitTest_nonunit line 33
4. theorem OAI.Ostmann.Arithmetic.PrimeCellReplacement.finite_product_prior_partition line 43
5. abbrev OAI.Ostmann.Arithmetic.PrimeCellReplacement.PrimeCellTuple line 63
6. def OAI.Ostmann.Arithmetic.PrimeCellReplacement.jointComplexTestSum line 66
7. theorem OAI.Ostmann.Arithmetic.PrimeCellReplacement.jointComplexTestSum_eq line 72