Structure OrderRingIso

Modification history

2025-08-18 09:17

Mathlib/Algebra/Order/Hom/Ring.lean

chore(Algebra): more porting notes for Algebra (#28409) …

Modified OrderRingIso View on Github →

2023-08-10 19:52

Mathlib/Algebra/Order/Hom/Ring.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified OrderRingIso View on Github →

2023-02-27 13:48

Mathlib/Algebra/Order/Hom/Ring.lean

feat: port Algebra.Order.Hom.Ring (#1482) …

Added OrderRingIso View on Github →