OAI/NumberTheory/Ostmann/Construction/RowCongruence.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Construction.unit_fraction_eq_iffline 8 - theorem
OAI.Ostmann.Construction.modFraction_eq_iff_reversal_dvdline 32 - theorem
OAI.Ostmann.Construction.modFraction_eq_iff_exists_unique_frequencyline 42 - theorem
OAI.Ostmann.Construction.reversal_frequency_ne_zeroline 60