OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualPrincipalBlockFamilyOuterMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerMass line 21
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerMass_nonneg line 26
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawMass_eq_outerMass_mul_bulkMass line 34
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.originalDrawMass_ne_zero_iff line 50
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerMass_ne_zero_nonbulk line 58
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualPrincipalBlockFamily.outerMass_ne_zero_block line 64