chore(Algebra/CharP/Two): reduce dependencies (leanprover-community#34663)

---
<!-- Your PR title will become the first line of the commit message.

In this box, the text above the `---` (if not empty) will be appended
to the commit message, and can be used to give additional context or
details. Please leave a blank newline before the `---`, otherwise GitHub
will format the text above it as a title.

For details on the "pull request lifecycle" in mathlib, please see:
https://leanprover-community.github.io/contribute/index.html

In particular, note that most reviewers will only notice your PR
if it passes the continuous integration checks.
Please ask for help on https://leanprover.zulipchat.com if needed.

When merging, all the commits will be squashed into a single commit
listing all co-authors.

Co-authors in the squash commit are gathered from two sources:

First, all authors of commits to this PR branch are included. Thus,
one way to add co-authors is to include at least one commit authored by
each co-author among the commits in the pull request. If necessary, you
may create empty commits to indicate co-authorship, using commands like so:

git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"

Second, co-authors can also be listed in lines at the very bottom of
the commit message (that is, directly before the `---`) using the following format:


If you are moving or deleting declarations, please include these lines
at the bottom of the commit message (before the `---`, and also before
any "Co-authored-by" lines) using the following format:

Moves:
- Vector.* -> List.Vector.*
- ...

Deletions:
- Nat.bit1_add_bit1
- ...

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

-->

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Author Name <author@email.com>

Author: astrainfinita

Mathlib/Algebra/CharP/Lemmas.lean

@@ -310,7 +310,7 @@ end CharP
 /-
 Preliminary definitions and results for the Frobenius map.
 Necessary here for simple results about sums of `p`-powers that are used in files forbidding
-to import algebra-related definitions (see `Mathlib/Algebra/CharP/Two.lean`).
+to import algebra-related definitions.
 -/
 section Frobenius
 

Mathlib/Algebra/CharP/Two.lean

@@ -5,8 +5,9 @@ Authors: Eric Wieser
 -/
 module
 
-public import Mathlib.Algebra.CharP.Lemmas
-public import Mathlib.GroupTheory.OrderOfElement
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Algebra.CharP.Defs
+public import Mathlib.Algebra.Ring.Parity
 
 /-!
 # Lemmas about rings of characteristic two
@@ -19,7 +20,10 @@ elsewhere, with a shorter name for ease of discovery, and no need for a `[Fact (
 
 public section
 
-assert_not_exists Algebra LinearMap
+-- TODO: `assert_not_exists Field` is added because of `Mathlib.GroupTheory.OrderOfElement`.
+-- If you want to import fields here, please refactor the import hierarchy for
+-- `Mathlib.GroupTheory.OrderOfElement`.
+assert_not_exists Algebra LinearMap Field
 
 variable {R ι : Type*}
 
@@ -48,10 +52,10 @@ section Semiring
 variable [Semiring R] [CharP R 2]
 
 @[scoped simp]
-theorem add_self_eq_zero (x : R) : x + x = 0 := by rw [← two_smul R x, two_eq_zero, zero_smul]
+theorem add_self_eq_zero (x : R) : x + x = 0 := by rw [← two_mul x, two_eq_zero, zero_mul]
 
 @[scoped simp]
-protected theorem two_nsmul (x : R) : 2 • x = 0 := by rw [two_smul, add_self_eq_zero]
+protected theorem two_nsmul (x : R) : 2 • x = 0 := by rw [two_nsmul, add_self_eq_zero]
 
 @[scoped simp]
 protected theorem add_cancel_left (a b : R) : a + (a + b) = b := by
@@ -96,26 +100,32 @@ section CommSemiring
 
 variable [CommSemiring R] [CharP R 2]
 
-theorem add_sq (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 :=
-  add_pow_char _ _ _
+theorem add_sq (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
+  simp [add_pow_two, two_eq_zero (R := R)]
 
 theorem add_mul_self (x y : R) : (x + y) * (x + y) = x * x + y * y := by
   rw [← pow_two, ← pow_two, ← pow_two, add_sq]
 
+/-- See `frobenius` for the Frobenius map. -/
+private def sqAddMonoidHom : R →+ R where
+  toFun := (· ^ 2)
+  map_zero' := zero_pow two_ne_zero
+  map_add' := add_sq
+
 theorem list_sum_sq (l : List R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
-  list_sum_pow_char _ _
+  map_list_sum sqAddMonoidHom _
 
 theorem list_sum_mul_self (l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum := by
   simp_rw [← pow_two, list_sum_sq]
 
 theorem multiset_sum_sq (l : Multiset R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
-  multiset_sum_pow_char _ _
+  map_multiset_sum sqAddMonoidHom _
 
 theorem multiset_sum_mul_self (l : Multiset R) :
     l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum := by simp_rw [← pow_two, multiset_sum_sq]
 
 theorem sum_sq (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2 :=
-  sum_pow_char _ _ _
+  map_sum sqAddMonoidHom _ _
 
 theorem sum_mul_self (s : Finset ι) (f : ι → R) :
     ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i := by simp_rw [← pow_two, sum_sq]
@@ -147,25 +157,4 @@ theorem neg_one_eq_one_iff [Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2 := b
   rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
   exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one
 
-@[simp]
-theorem orderOf_neg_one [Nontrivial R] : orderOf (-1 : R) = if ringChar R = 2 then 1 else 2 := by
-  split_ifs with h
-  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
-  apply orderOf_eq_prime
-  · simp
-  simpa [neg_one_eq_one_iff] using h
-
 end ringChar
-
-section CharP
-
-variable [Ring R]
-
-lemma CharP.orderOf_eq_two_iff [Nontrivial R] [NoZeroDivisors R] (p : ℕ)
-    (hp : p ≠ 2) [CharP R p] {x : R} : orderOf x = 2 ↔ x = -1 := by
-  simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
-    and_iff_left_iff_imp]
-  rintro rfl
-  exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))
-
-end CharP

Mathlib/Data/Nat/Totient.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes
 module
 
 public import Mathlib.Algebra.CharP.Two
+public import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
 public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 public import Mathlib.Data.Nat.Cast.Field
 public import Mathlib.Data.Nat.Factorization.Basic

Mathlib/GroupTheory/OrderOfElement.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Julian Kuelshammer
 -/
 module
 
-public import Mathlib.Algebra.CharP.Defs
+public import Mathlib.Algebra.CharP.Two
 public import Mathlib.Algebra.Group.Commute.Basic
 public import Mathlib.Algebra.Group.Pointwise.Set.Finite
 public import Mathlib.Algebra.Group.Subgroup.Finite
@@ -520,6 +520,22 @@ theorem exists_orderOf_eq_prime_pow_iff :
     obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
     exact ⟨k, hk⟩⟩
 
+@[simp]
+theorem orderOf_neg_one {R} [Ring R] [Nontrivial R] :
+    orderOf (-1 : R) = if ringChar R = 2 then 1 else 2 := by
+  split_ifs with h
+  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
+  apply orderOf_eq_prime
+  · simp
+  simpa [neg_one_eq_one_iff] using h
+
+lemma CharP.orderOf_eq_two_iff {R} [Ring R] [Nontrivial R] [NoZeroDivisors R] (p : ℕ)
+    (hp : p ≠ 2) [CharP R p] {x : R} : orderOf x = 2 ↔ x = -1 := by
+  simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
+    and_iff_left_iff_imp]
+  rintro rfl
+  exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))
+
 end PPrime
 
 /-- The equivalence between `Fin (orderOf x)` and `Submonoid.powers x`, sending `i` to `x ^ i` -/

Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

@@ -375,7 +375,7 @@ theorem isCoatom_stabilizer_of_ncard_lt_ncard_compl
     apply hB.eq_univ_of_card_lt
     have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
     rw [← Set.ncard_add_ncard_compl s]
-    linarith
+    lia
   -- The proof needs 4 steps
   /- Step 1 : `sᶜ` is not a block.
        This uses that `Nat.card s < Nat.card sᶜ`.

Mathlib/GroupTheory/RegularWreathProduct.lean

@@ -5,10 +5,10 @@ Authors: Francisco Silva
 -/
 module
 
-public import Mathlib.GroupTheory.Sylow
 public import Mathlib.Algebra.Group.PUnit
 public import Mathlib.Data.Finite.Perm
-public import Mathlib.Algebra.Group.End
+public import Mathlib.Data.Nat.Multiplicity
+public import Mathlib.GroupTheory.Sylow
 
 /-!
 # Regular wreath product

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -13,6 +13,7 @@ public import Mathlib.Data.ZMod.QuotientGroup
 public import Mathlib.GroupTheory.Exponent
 public import Mathlib.GroupTheory.Subgroup.Simple
 public import Mathlib.Tactic.Group
+public import Mathlib.Tactic.IntervalCases
 
 /-!
 # Cyclic groups

Mathlib/RingTheory/IntegralDomain.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Chris Hughes
 module
 
 public import Mathlib.Algebra.Polynomial.Roots
+public import Mathlib.Algebra.Ring.GeomSum
 public import Mathlib.Data.Fintype.Inv
 public import Mathlib.GroupTheory.SpecificGroups.Cyclic
 public import Mathlib.Tactic.FieldSimp