OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairedFrequencyAverageRingUnit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.bulk_ring_unit_giant_average_le line 13
2. def OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.canonicalRingUnitBulkAverage line 28
3. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.canonicalRingUnitBulkAverage_le_weight line 39
4. theorem OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.sum_supported_ringUnit_average_le_total line 52