Zulip Chat Archive
Stream: mathlib4
Topic: SubringClass
Violeta Hernández (Nov 28 2025 at 14:20):
Mathlib has docs#Subring.toIsOrderedRing which shows that a subring of an ordered ring is itself an ordered ring. I'd like to use this for a docs#ValuationSubring. Is the correct thing to do here to generalize that instance to SubringClass?
Junyan Xu (Nov 28 2025 at 14:21):
Yes but do you mean docs#ValuationSubring
Last updated: Dec 20 2025 at 21:32 UTC