OAI/NumberTheory/Ostmann/Construction/OffDiagonalReindex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.pivotPairWeight line 12
2. theorem OAI.Ostmann.Construction.pivotPairWeight_nonzero line 23
3. theorem OAI.Ostmann.Construction.mem_frequency_range_of_natAbs_le line 38
4. theorem OAI.Ostmann.Construction.pivotPair_frequency_reindex line 44