OAI/NumberTheory/JointDickman/Probability/SubsetKernelProductLaw.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The finite retention-kernel mean as a signed integer-product law
- theorem
OAI.JointDickman.subsetKernel_product_meanline 12