[Merged by Bors] - feat: Galois groups of finite fields

[alreadydone]

---

[github-actions]

PR summary 394f7c27ea

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card	1535	1479	-56 (-3.65%)
Mathlib.FieldTheory.Finite.Basic	1486	1507	+21 (+1.41%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card	-56
8 files Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Complete Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.Isocrystal	3
Mathlib.RingTheory.RootsOfUnity.Minpoly	8
Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.LSeries.Dirichlet	11
11 files Mathlib.FieldTheory.Finite.Polynomial Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung	16
Mathlib.NumberTheory.DirichletCharacter.Orthogonality	20
14 files Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Finite.Basic Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.SumTwoSquares Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity	21

---

Declarations diff

+ IsOfFinOrder.pow_eq_pow_iff_modEq
+ IsOfFinOrder.pow_inj_mod
+ _root_.Module.card_eq_pow_finrank
+ _root_.card_eq_pow_finrank
+ bijective_frobeniusAlgEquivOfAlgebraic_pow
+ bijective_frobeniusAlgHom_pow
+ bijective_of_subsingleton
+ coe_frobeniusAlgEquivOfAlgebraic
+ coe_frobeniusAlgHom
+ frobeniusAlgEquiv
+ frobeniusAlgEquivOfAlgebraic
+ frobeniusAlgHom
+ instance (K L) [Finite L] [Field K] [Field L] [Algebra K L] : IsCyclic (L ≃ₐ[K] L)
+ iterateFrobenius_eq_pow
+ orderOf_frobeniusAlgEquivOfAlgebraic
+ orderOf_frobeniusAlgHom
++ coe_pow
- card_eq_pow_finrank

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

[riccardobrasca]

I left a couple of comments to code that you moved, feel free to ignore them if you think they don't fit in this PR.

[mathlib-bors]

✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[leanprover-community-mathlib4-bot]

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style