[Merged by Bors] - feat: radical lemmas for natural numbers and integers

[Parcly-Taxel]

These are needed as part of a project I'm doing for my PhD under Frank Stephan.

[github-actions]

PR summary 592989bdba

Import changes exceeding 2%

%	File
+28.28%	Mathlib.RingTheory.Radical.NatInt

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Radical.NatInt	916	1175	+259 (+28.28%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Radical.NatInt	259
Mathlib.RingTheory.Radical (new file)	1176

---

Declarations diff

+ UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs
+ radical_natAbs_eq_radical
+ self_lt_radical_iff
++ radical_eq_one_iff
++ radical_eq_prod_primeFactors
++- one_lt_radical_iff
++- radical_le_one_iff
++- radical_pos
++- two_le_radical_iff

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[vihdzp]

This is quite a large import change. Maybe we could have Mathlib.RingTheory.Radical.Basic with the existing material and Mathlib.RingTheory.Radical.Int with the new lemmas?

[Parcly-Taxel]

This is quite a large import change. Maybe we could have Mathlib.RingTheory.Radical.Basic with the existing material and Mathlib.RingTheory.Radical.Int with the new lemmas?

I had that in mind, but should Mathlib.RingTheory.Radical.Int also include the lemmas specific to Nat?

[Parcly-Taxel]

This is quite a large import change. Maybe we could have Mathlib.RingTheory.Radical.Basic with the existing material and Mathlib.RingTheory.Radical.Int with the new lemmas?

OK, done.

[vihdzp]

I think the idea is that in your first PR you just move the file entirely, and in a follow-up PR you add deprecated_module. That way the diff stays small.

[Parcly-Taxel]

I think the idea is that in your first PR you just move the file entirely, and in a follow-up PR you add deprecated_module. That way the diff stays small.

Done.

[vihdzp]

LGTM, just some minor style/grammar remarks.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[riccardobrasca]

If I understand correctly you are splitting a file and also adding stuff. Can you please open a PR only with the splitting? Thanks!

[Parcly-Taxel]

If I understand correctly you are splitting a file and also adding stuff. Can you please open a PR only with the splitting? Thanks!

#36098 does the splitting.

[riccardobrasca]

!radar

[leanprover-radar]

Benchmark results for 78b4420 against 592989b are in! @riccardobrasca

• ✅ build//instructions: -5.3G (-0.00%)

No significant changes detected.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step