Commit 2025-01-20 08:54 c4510a08
View on Github →feat: make Sub ℝ≥0 and Sub ℝ≥0∞ computable (#20856)
This comes for free by relaxing some unnecessarily-strong typeclass requirements.
(as a reminder, LinearOrder NNReal is noncomputable as it contains noncomputable Decidable instances)