chore(Periodic): reduce imports

[YaelDillies]

---

• depends on: [Merged by Bors] - chore(Algebra/CharP/Basic): don't import IsSimpleRing #20550
• depends on: [Merged by Bors] - chore: move results about DivisionMonoid + HasDistribNeg #20551
• depends on: chore(Algebra/CharP/Defs): do not import Field #20566

[github-actions]

PR summary 4f60749999

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.CharP.Defs	420	398	-22 (-5.24%)
Mathlib.Algebra.CharP.Invertible	421	405	-16 (-3.80%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.CharP.Basic Mathlib.Algebra.CharP.Defs	-22
Mathlib.Data.Matrix.CharP Mathlib.Algebra.CharP.Pi	-21
Mathlib.Algebra.CharP.Invertible	-16
3 files Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Combinatorics.Additive.Corner.Defs	-10
Mathlib.Algebra.Ring.Periodic (new file)	903

---

Declarations diff

+ Antiperiodic
+ Antiperiodic.add
+ Antiperiodic.add_const
+ Antiperiodic.add_int_mul_eq
+ Antiperiodic.add_nsmul_eq
+ Antiperiodic.add_zsmul_eq
+ Antiperiodic.const_add
+ Antiperiodic.const_inv_smul
+ Antiperiodic.const_inv_smul₀
+ Antiperiodic.const_smul
+ Antiperiodic.const_smul₀
+ Antiperiodic.const_sub
+ Antiperiodic.div
+ Antiperiodic.eq
+ Antiperiodic.even_nsmul_periodic
+ Antiperiodic.even_zsmul_periodic
+ Antiperiodic.funext
+ Antiperiodic.funext'
+ Antiperiodic.int_even_mul_periodic
+ Antiperiodic.int_mul_eq_of_eq_zero
+ Antiperiodic.int_mul_sub_eq
+ Antiperiodic.int_odd_mul_antiperiodic
+ Antiperiodic.mul
+ Antiperiodic.nat_even_mul_periodic
+ Antiperiodic.nat_mul_eq_of_eq_zero
+ Antiperiodic.nat_odd_mul_antiperiodic
+ Antiperiodic.neg
+ Antiperiodic.neg_eq
+ Antiperiodic.nsmul_sub_eq
+ Antiperiodic.odd_nsmul_antiperiodic
+ Antiperiodic.odd_zsmul_antiperiodic
+ Antiperiodic.periodic
+ Antiperiodic.periodic_two_mul
+ Antiperiodic.smul
+ Antiperiodic.sub
+ Antiperiodic.sub_const
+ Antiperiodic.sub_eq
+ Antiperiodic.sub_eq'
+ Antiperiodic.sub_int_mul_eq
+ Antiperiodic.sub_nsmul_eq
+ Antiperiodic.sub_zsmul_eq
+ Antiperiodic.zsmul_sub_eq
+ Periodic
+ Periodic.add_antiperiod
+ Periodic.add_antiperiod_eq
+ Periodic.add_const
+ Periodic.add_period
+ Periodic.comp
+ Periodic.comp_addHom
+ Periodic.const_add
+ Periodic.const_inv_smul
+ Periodic.const_inv_smul₀
+ Periodic.const_mul
+ Periodic.const_smul
+ Periodic.const_smul₀
+ Periodic.const_sub
+ Periodic.div
+ Periodic.eq
+ Periodic.funext
+ Periodic.int_mul
+ Periodic.int_mul_eq
+ Periodic.int_mul_sub_eq
+ Periodic.lift
+ Periodic.lift_coe
+ Periodic.map_vadd_multiples
+ Periodic.map_vadd_zmultiples
+ Periodic.mul
+ Periodic.nat_mul
+ Periodic.nat_mul_eq
+ Periodic.nat_mul_sub_eq
+ Periodic.neg
+ Periodic.neg_eq
+ Periodic.neg_nat_mul
+ Periodic.neg_nsmul
+ Periodic.not_injective
+ Periodic.nsmul
+ Periodic.nsmul_eq
+ Periodic.nsmul_sub_eq
+ Periodic.smul
+ Periodic.sub_antiperiod
+ Periodic.sub_antiperiod_eq
+ Periodic.sub_const
+ Periodic.sub_eq
+ Periodic.sub_eq'
+ Periodic.sub_int_mul_eq
+ Periodic.sub_nat_mul_eq
+ Periodic.sub_nsmul_eq
+ Periodic.sub_period
+ Periodic.sub_zsmul_eq
+ Periodic.zsmul
+ Periodic.zsmul_eq
+ Periodic.zsmul_sub_eq
+ _root_.Finset.periodic_prod
+ _root_.List.periodic_prod
+ _root_.Multiset.periodic_prod
+ periodic_with_period_zero

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.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
4817	-1	porting notes

Current commit 4f60749999
Reference commit 60ae2db33d

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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/CharP/Basic): don't import IsSimpleRing #20550
• [Merged by Bors] - chore: move results about DivisionMonoid + HasDistribNeg #20551
• chore(Algebra/CharP/Defs): do not import Field #20566
  By Dependent Issues (🤖). Happy coding!