Def Subring.orderedSubtype

Modification history

2025-04-10 16:38
Mathlib/Algebra/Ring/Subring/Order.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified Subring.orderedSubtypeView on Github →
2024-02-26 23:59
Mathlib/RingTheory/Subring/Order.lean
feat: lemmas about germs in topological spaces (#9747) …
Added Subring.orderedSubtypeView on Github →