[Merged by Bors] - chore(Algebra/Ring): shortcut IsDomain instances for Nat and Int

[YaelDillies]

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

---

[github-actions]

PR summary 0d837987e5

Import changes exceeding 2%

%	File
+7.88%	Mathlib.Algebra.Ring.Int.Defs
+14.81%	Mathlib.Algebra.Ring.Nat

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Ring.Nat	135	155	+20 (+14.81%)
Mathlib.Algebra.Ring.Int.Defs	165	178	+13 (+7.88%)

Import changes for all files

Files	Import difference
8 files Mathlib.Algebra.CharZero.AddMonoidHom Mathlib.Algebra.Group.NatPowAssoc Mathlib.Algebra.Order.Ring.Unbundled.Rat Mathlib.Data.FP.Basic Mathlib.Data.Int.Bitwise Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.LeastGreatest Mathlib.Data.Nat.Cast.Basic	1
Mathlib.Algebra.Ring.Int.Units	8
Mathlib.Data.Int.NatAbs	11
Mathlib.Algebra.Homology.Embedding.Basic	12
Mathlib.Algebra.Ring.Int.Defs Mathlib.Data.Int.Cast.Field	13
Mathlib.Algebra.Ring.Nat	20

---

Declarations diff

++ instIsDomain

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jcommelin]

This is causing quite an import increase in rather low-level files. Is there a different reorganization that makes sense? Possibly even a new file?

[YaelDillies]

Only 5 files see a significant import increase. Do you not think that's fine?

I personally think it makes a lot of sense that Algebra.Ring.Foo imports Data.Foo.Basic

[kim-em]

Yeah, let's go.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Lint style
• Build