Theorem Dyadic.toRat_one

Modification history

2026-11-10 12:28
Mathlib/Data/Dyadic/Basic.lean
feat: `Dyadic` is an ordered ring (#43038) …
Added Dyadic.toRat_oneView on Github →