Commit 2026-11-10 12:28 b1cf5e59

View on Github →

feat: Dyadic is an ordered ring (#43038) Prove Dyadic is a linearly ordered ring, providing instances for LinearOrder, CommRing, and IsStrictOrderedRing. Remove corresponding material from Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Dyadic. Follow-up to #45186.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dyadic/Basic.lean

added theorem Dyadic.intCast_natCast

added theorem Dyadic.toRat_one

Modified Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Dyadic.lean