Zulip Chat Archive

Stream: new members

Topic: unknown identifier 'ordered_ring'


Nico Courts (Jun 13 2020 at 22:03):

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 (Jun 13 2020 at 22:07):

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 (Jun 13 2020 at 22:08):

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

Nico Courts (Jun 13 2020 at 22:09):

Awesome! Thank you.

Bryan Gin-ge Chen (Jun 13 2020 at 22:09):

Let's see if this works: docs#ordered_ring

Nico Courts (Jun 13 2020 at 22:14):

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


Last updated: Dec 20 2023 at 11:08 UTC