Skip to content

Commit dbaddce

Browse files
ChrisHughes24joneugsterurkud
committed
feat: port Algebra.Order.Nonneg.Ring (#1260)
Really difficult to diagnose timeout here Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
1 parent e859907 commit dbaddce

File tree

2 files changed

+410
-0
lines changed

2 files changed

+410
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,7 @@ import Mathlib.Algebra.Order.Monoid.Units
154154
import Mathlib.Algebra.Order.Monoid.WithTop
155155
import Mathlib.Algebra.Order.Monoid.WithZero.Basic
156156
import Mathlib.Algebra.Order.Monoid.WithZero.Defs
157+
import Mathlib.Algebra.Order.Nonneg.Ring
157158
import Mathlib.Algebra.Order.Pi
158159
import Mathlib.Algebra.Order.Pointwise
159160
import Mathlib.Algebra.Order.Positive.Field

0 commit comments

Comments
 (0)