Commit 2023-10-07 18:13 fd3a089b

View on Github →

feat(NumberTheory): Rayleigh's theorem (#7027)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Rayleigh.lean

added theorem Irrational.beattySeq'_pos_eq

added theorem Irrational.beattySeq_symmDiff_beattySeq_pos

added theorem beattySeq'_symmDiff_beattySeq_pos

added theorem beattySeq_symmDiff_beattySeq'_pos

added theorem compl_beattySeq'

added theorem compl_beattySeq