Revision #1224 → #2347 · back to history
modifiedFinite field5a7c62e5da1a
| Field | From #1224 | To #2347 |
|---|
| mathlib.decl | FiniteField | — |
| mathlib.match_kind | exact | — |
| note | A finite field is encoded in Mathlib as a type with `[Field K] [Finite K]` (or `[Fintype K]`); the namespace `FiniteField` in `Mathlib/FieldTheory/Finite/Basic.lean` collects results under this assumption. | Mathlib encodes finite fields via the combination of the typeclasses `[Field K] [Finite K]` (or `[Fintype K]`); there is no dedicated `FiniteField` definition decl, but the `FiniteField` namespace in `Mathlib/FieldTheory/Finite/Basic.lean` collects all results under this assumption. |
modifiedOrder of a finite field5f4b62d0e2b4
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.FieldTheory.Finite.Basic | Mathlib.Data.Fintype.Card |
| note | The order is just the cardinality `Fintype.card K` / `Nat.card K`; throughout `FiniteField` it is the abbreviation `q`. | The order is the cardinality `Fintype.card K` (alias `Nat.card K`); throughout `FiniteField` results it is abbreviated `q`. |
modifiedOrder/size of a finite field (Properties)f7195db03113
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.FieldTheory.Finite.Basic | Mathlib.Data.Fintype.Card |
modifiedCharacterization of orders of finite fieldscfefc57ce4a6
| Field | From #1224 | To #2347 |
|---|
| note | `FiniteField.card` (and `FiniteField.card'`, `FiniteField.isPrimePow_card`) states that any finite field has cardinality a prime power. | `FiniteField.card` (with `FiniteField.card'` and `FiniteField.isPrimePow_card`) states that any finite field has cardinality a prime power. |
modifiedPrimitive element1e9b71ac638a
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.GroupTheory.SpecificGroups.Cyclic | Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic |
| note | Mathlib expresses primitive elements through `IsCyclic.exists_generator` on `Kˣ`; there is no dedicated `primitiveElement` name for finite fields. | Mathlib expresses primitive elements via `IsCyclic.exists_generator` on `Kˣ`; there is no dedicated `primitiveElement` name for finite fields. |
modifiedFreshman's dream identity157ee12b9b2e
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.Algebra.CharP.Frobenius | Mathlib.Algebra.CharP.Lemmas |
modifiedChevalley–Warning: finite fields are quasi-algebraically closed28a1a508753a
| Field | From #1224 | To #2347 |
|---|
| note | Chevalley–Warning is formalized as `char_dvd_card_solutions_of_sum_lt`, but the abstract notion of a quasi-algebraically closed (C₁) field is not defined in Mathlib. | Chevalley–Warning itself is formalized as `char_dvd_card_solutions_of_sum_lt`, but the abstract notion of a quasi-algebraically closed (C₁) field is not defined in Mathlib. |
modifiedUniqueness up to isomorphism via splitting fieldsd81bf196db30
| Field | From #1224 | To #2347 |
|---|
| note | `GaloisField.algEquivGaloisField` (and `FiniteField.algEquivOfCardEq`) realize this via the universal property of `IsSplittingField.algEquiv`. | `GaloisField.algEquivGaloisField` (with `FiniteField.algEquivOfCardEq`) realizes this via the universal property of the splitting field. |
modifiedFrobenius automorphism on GF(4)db5ab40ef482
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.Algebra.CharP.Frobenius | Mathlib.Algebra.CharP.Lemmas |
modifiedPrimitive element of GF(q)7126616fa3c2
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.GroupTheory.SpecificGroups.Cyclic | Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic |
modifiedExistence criterion for primitive n-th roots of unity in GF(q)7df0e8b00ca9
| Field | From #1224 | To #2347 |
|---|
| note | Follows from cyclicity of `Kˣ` and `IsCyclic.card_orderOf_eq_totient` plus `Fintype.card_units = q - 1`, but no dedicated `IsPrimitiveRoot.exists ↔ n ∣ q-1` for finite fields is isolated. | Follows from cyclicity of `Kˣ` and `IsCyclic.card_orderOf_eq_totient` together with `Fintype.card_units = q - 1`, but no dedicated `∃ ζ, IsPrimitiveRoot ζ n ↔ n ∣ q-1` is isolated. |
modifiedNo primitive p-th roots of unity in characteristic p817f436cac78
| Field | From #1224 | To #2347 |
|---|
| mathlib.decl | frobenius_zmod | ZMod.frobenius_zmod |
| note | Follows from `a^p = a` (`ZMod.pow_card`/`FiniteField.pow_card`), but no isolated statement that there are no primitive `p`-th roots of unity in characteristic `p` was found. | Follows from `a^p = a` (`ZMod.pow_card`/`FiniteField.pow_card`) and `ZMod.frobenius_zmod`, but no isolated statement that there are no primitive `p`-th roots of unity in characteristic `p` was found. |
modifiedFrobenius automorphism7101e2d8422d
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.Algebra.CharP.Frobenius | Mathlib.Algebra.CharP.Lemmas |
modifiedGalois group of GF(p^n)/GF(p) is cyclic of order nb0f393b69844
| Field | From #1224 | To #2347 |
|---|
| note | Combined with the `IsCyclic Gal(L/K)` instance for finite extensions of finite fields (in `Basic.lean`) and `IsGalois.card_aut_eq_finrank`, this gives the full statement. | Combined with the `IsCyclic Gal(L/K)` instance for finite extensions of finite fields and `IsGalois.card_aut_eq_finrank`, this gives the full statement. |
addedGF(p^n) is a Galois extension of GF(p) with cyclic Galois group5ac4bec4d11a
modifiedIrreducible polynomial over a finite fieldad58cbc3b19b
| Field | From #1224 | To #2347 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Irreducible | Mathlib.Algebra.Group.Irreducible.Defs |