unknown identifier 'ordered_ring'

Stream: new members

[Nico Courts]

Hey! I am working through the "Theorem Proving in Lean" document and ran into an issue. I used leanpackage to just get the most recent community version of Lean (3.16.2, I believe) and when I type the following line : variables (real : Type) [ordered_ring real] I get the above error. I believe I have fixed things by downgrading lean via the leanpkg.toml file, so it should work for now.

Is there a way to make this work with the more recent community release, though? Did the syntax just change? Is a new open needed now? Thanks!

[Kevin Buzzard]

It might have been moved into mathlib. If you're using VS code you can search for ordered_ring and find where it ended up. It'll just be an import you're missing

[Kevin Buzzard]

Recently a bunch of algebra got moved out of core into mathlib

[Nico Courts]

Awesome! Thank you.

[Bryan Gin-ge Chen]

Let's see if this works: docs#ordered_ring

[Nico Courts]

Yup! import algebra.ordered_ring did the trick! Thanks to both of you.