Commit 2025-10-28 10:18 1089256c
View on Github →chore(Algebra/Ring): shortcut IsDomain instances for Nat and Int (#30713)
These instances are currently inferred from the IsStrictOrderedRing ones (see code snippet), but in #30563 I need these instances earlier than the IsStrictOrderedRing ones.
import Mathlib
#synth IsDomain ℕ -- IsStrictOrderedRing.isDomain
#synth IsDomain ℤ -- IsStrictOrderedRing.isDomain