Theorem compl_beattySeq

Modification history

2025-03-27 13:33

Mathlib/NumberTheory/Rayleigh.lean

refactor: merge API for `ENNReal.HolderConjugate` and `{E}{NN}Real.IsConjExponent` (#22944) …

Modified compl_beattySeq View on Github →

2024-02-17 09:43

Mathlib/NumberTheory/Rayleigh.lean

feat: Conjugate exponents in `ℝ≥0` (#10589) …

Modified compl_beattySeq View on Github →

2023-10-07 18:13

Mathlib/NumberTheory/Rayleigh.lean

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

Added compl_beattySeq View on Github →