chore: split Algebra.CharP.Basic, reduce imports in RingTheory.Multip…

…licity (#8637)

This was adding unnecessary imports to `Data.ZMod.Basic`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Counterexamples/CharPZeroNeCharZero.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Eric Wieser
 -/
 import Mathlib.Algebra.CharP.Basic
+import Mathlib.Algebra.PUnitInstances
 
 #align_import char_p_zero_ne_char_zero from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 

Mathlib.lean

@@ -104,6 +104,7 @@ import Mathlib.Algebra.CharP.LocalRing
 import Mathlib.Algebra.CharP.MixedCharZero
 import Mathlib.Algebra.CharP.Pi
 import Mathlib.Algebra.CharP.Quotient
+import Mathlib.Algebra.CharP.Reduced
 import Mathlib.Algebra.CharP.Subring
 import Mathlib.Algebra.CharP.Two
 import Mathlib.Algebra.CharZero.Defs
@@ -3121,6 +3122,7 @@ import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.RingTheory.Valuation.ExtendToLocalization
 import Mathlib.RingTheory.Valuation.Integers
 import Mathlib.RingTheory.Valuation.Integral
+import Mathlib.RingTheory.Valuation.PrimeMultiplicity
 import Mathlib.RingTheory.Valuation.Quotient
 import Mathlib.RingTheory.Valuation.RamificationGroup
 import Mathlib.RingTheory.Valuation.ValuationRing

Mathlib/Algebra/CharP/Basic.lean

@@ -5,8 +5,10 @@ Authors: Kenny Lau, Joey van Langen, Casper Putz
 -/
 import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Nat.Multiplicity
+import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.Data.Nat.Cast.Prod
+import Mathlib.Algebra.Group.ULift
 import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.RingTheory.Nilpotent
 
 #align_import algebra.char_p.basic from "leanprover-community/mathlib"@"47a1a73351de8dd6c8d3d32b569c8e434b03ca47"
 
@@ -439,23 +441,6 @@ end CommRing
 
 end frobenius
 
-theorem frobenius_inj [CommRing R] [IsReduced R] (p : ℕ) [Fact p.Prime] [CharP R p] :
-    Function.Injective (frobenius R p) := fun x h H => by
-  rw [← sub_eq_zero] at H ⊢
-  rw [← frobenius_sub] at H
-  exact IsReduced.eq_zero _ ⟨_, H⟩
-#align frobenius_inj frobenius_inj
-
-/-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
-then every `a : R` is a square. -/
-theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2]
-    (a : R) : IsSquare a := by
-  cases nonempty_fintype R
-  exact
-    Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
-      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)
-#align is_square_of_char_two' isSquare_of_charTwo'
-
 namespace CharP
 
 section
@@ -492,23 +477,6 @@ theorem ringChar_zero_iff_CharZero [NonAssocRing R] : ringChar R = 0 ↔ CharZer
 
 end
 
-section CommRing
-
-variable [CommRing R] [IsReduced R] {R}
-
-@[simp]
-theorem pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [Fact p.Prime] [CharP R p] (x : R) :
-    x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 := by
-  induction' k with k hk
-  · rw [pow_zero, one_mul]
-  · refine' ⟨fun h => _, fun h => _⟩
-    · rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h
-      exact hk.1 (frobenius_inj R p h)
-    · rw [pow_mul', h, one_pow]
-#align char_p.pow_prime_pow_mul_eq_one_iff CharP.pow_prime_pow_mul_eq_one_iff
-
-end CommRing
-
 section Semiring
 
 variable [NonAssocSemiring R]

Mathlib/Algebra/CharP/Quotient.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Eric Wieser
 -/
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Operations
 
 #align_import algebra.char_p.quotient from "leanprover-community/mathlib"@"85e3c05a94b27c84dc6f234cf88326d5e0096ec3"
 

Mathlib/Algebra/CharP/Reduced.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Joey van Langen, Casper Putz
+-/
+import Mathlib.Algebra.CharP.Basic
+import Mathlib.RingTheory.Nilpotent
+
+#align_import algebra.char_p.basic from "leanprover-community/mathlib"@"47a1a73351de8dd6c8d3d32b569c8e434b03ca47"
+
+/-!
+# Results about characteristic p reduced rings
+-/
+
+
+open Finset
+
+open BigOperators
+
+theorem frobenius_inj (R : Type*) [CommRing R] [IsReduced R] (p : ℕ) [Fact p.Prime] [CharP R p] :
+    Function.Injective (frobenius R p) := fun x h H => by
+  rw [← sub_eq_zero] at H ⊢
+  rw [← frobenius_sub] at H
+  exact IsReduced.eq_zero _ ⟨_, H⟩
+#align frobenius_inj frobenius_inj
+
+/-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
+then every `a : R` is a square. -/
+theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2]
+    (a : R) : IsSquare a := by
+  cases nonempty_fintype R
+  exact
+    Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
+      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)
+#align is_square_of_char_two' isSquare_of_charTwo'
+
+namespace CharP
+
+variable {R : Type*} [CommRing R] [IsReduced R]
+
+@[simp]
+theorem pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [Fact p.Prime] [CharP R p] (x : R) :
+    x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 := by
+  induction' k with k hk
+  · rw [pow_zero, one_mul]
+  · refine' ⟨fun h => _, fun h => _⟩
+    · rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h
+      exact hk.1 (frobenius_inj R p h)
+    · rw [pow_mul', h, one_pow]
+#align char_p.pow_prime_pow_mul_eq_one_iff CharP.pow_prime_pow_mul_eq_one_iff
+
+end CharP

Mathlib/Data/ZMod/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Algebra.CharP.Basic
+import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Data.Fintype.Units
 import Mathlib.Data.Nat.Parity
 import Mathlib.Tactic.FinCases

Mathlib/FieldTheory/Finite/Basic.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Joey van Langen, Casper Putz
 -/
 import Mathlib.FieldTheory.Separable
 import Mathlib.RingTheory.IntegralDomain
+import Mathlib.Algebra.CharP.Reduced
 import Mathlib.Tactic.ApplyFun
 
 #align_import field_theory.finite.basic from "leanprover-community/mathlib"@"12a85fac627bea918960da036049d611b1a3ee43"

Mathlib/FieldTheory/Perfect.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.Construction
+import Mathlib.Algebra.CharP.Reduced
 
 /-!
 

Mathlib/NumberTheory/Padics/PadicNumbers.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
+import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.NumberTheory.Padics.PadicNorm
 import Mathlib.Analysis.Normed.Field.Basic
 

Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

@@ -5,8 +5,7 @@ Authors: Kevin Buzzard
 -/
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.Ideal.LocalRing
-import Mathlib.RingTheory.Multiplicity
-import Mathlib.RingTheory.Valuation.Basic
+import Mathlib.RingTheory.Valuation.PrimeMultiplicity
 import Mathlib.LinearAlgebra.AdicCompletion
 
 #align_import ring_theory.discrete_valuation_ring.basic from "leanprover-community/mathlib"@"c163ec99dfc664628ca15d215fce0a5b9c265b68"

Mathlib/RingTheory/Multiplicity.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Chris Hughes
 -/
 import Mathlib.Algebra.Associated
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.RingTheory.Valuation.Basic
+import Mathlib.Algebra.SMulWithZero
+import Mathlib.Data.Nat.PartENat
+import Mathlib.Tactic.Linarith
 
 #align_import ring_theory.multiplicity from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
@@ -623,23 +624,6 @@ theorem multiplicity_pow_self_of_prime {p : α} (hp : Prime p) (n : ℕ) :
 
 end CancelCommMonoidWithZero
 
-section Valuation
-
-variable {R : Type*} [CommRing R] [IsDomain R] {p : R} [DecidableRel (Dvd.dvd : R → R → Prop)]
-
-/-- `multiplicity` of a prime in an integral domain as an additive valuation to `PartENat`. -/
-noncomputable def addValuation (hp : Prime p) : AddValuation R PartENat :=
-  AddValuation.of (multiplicity p) (multiplicity.zero _) (one_right hp.not_unit)
-    (fun _ _ => min_le_multiplicity_add) fun _ _ => multiplicity.mul hp
-#align multiplicity.add_valuation multiplicity.addValuation
-
-@[simp]
-theorem addValuation_apply {hp : Prime p} {r : R} : addValuation hp r = multiplicity p r :=
-  rfl
-#align multiplicity.add_valuation_apply multiplicity.addValuation_apply
-
-end Valuation
-
 end multiplicity
 
 section Nat

Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis, Chris Hughes
+-/
+import Mathlib.RingTheory.Multiplicity
+import Mathlib.RingTheory.Valuation.Basic
+
+/-!
+# `multiplicity` of a prime in an integral domain as an additive valuation
+-/
+
+variable {R : Type*} [CommRing R] [IsDomain R] {p : R} [DecidableRel (Dvd.dvd : R → R → Prop)]
+
+/-- `multiplicity` of a prime in an integral domain as an additive valuation to `PartENat`. -/
+noncomputable def multiplicity.addValuation (hp : Prime p) : AddValuation R PartENat :=
+  AddValuation.of (multiplicity p) (multiplicity.zero _) (one_right hp.not_unit)
+    (fun _ _ => min_le_multiplicity_add) fun _ _ => multiplicity.mul hp
+#align multiplicity.add_valuation multiplicity.addValuation
+
+@[simp]
+theorem multiplicity.addValuation_apply {hp : Prime p} {r : R} :
+    addValuation hp r = multiplicity p r :=
+  rfl
+#align multiplicity.add_valuation_apply multiplicity.addValuation_apply