Revision #2347 → #2994 · back to history
modifiedFinite field5a7c62e5da1a
| Field | From #2347 | To #2994 |
|---|
| note | 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. | Mathlib encodes finite fields via `[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 results under this assumption. |
modifiedOrder of a finite field5f4b62d0e2b4
| Field | From #2347 | To #2994 |
|---|
| note | The order is the cardinality `Fintype.card K` (alias `Nat.card K`); throughout `FiniteField` results it is abbreviated `q`. | The order is the cardinality `Fintype.card K`; throughout `FiniteField` results it is abbreviated `q`. |
modifiedExistence and isomorphism of finite fields by order1451f3a3c8b4
| Field | From #2347 | To #2994 |
|---|
| note | Existence is given by `GaloisField p n` with `GaloisField.card`, and uniqueness up to isomorphism by `FiniteField.algEquivOfCardEq` / `FiniteField.ringEquivOfCardEq`. | Existence via `GaloisField p n` with `GaloisField.card`, and uniqueness up to isomorphism by `FiniteField.algEquivOfCardEq`/`FiniteField.ringEquivOfCardEq`. |
modifiedUniqueness of finite fields of given order494efb277eff
| Field | From #2347 | To #2994 |
|---|
| note | Any two finite fields of equal cardinality are ring-isomorphic via `FiniteField.ringEquivOfCardEq` (and algebra-isomorphic via `FiniteField.algEquivOfCardEq`). | Any two finite fields of equal cardinality are ring-isomorphic via `FiniteField.ringEquivOfCardEq` (algebra-isomorphic via `FiniteField.algEquivOfCardEq`). |
modifiedMultiplicative group of a finite field is cyclic0eebcc5f46b2
| Field | From #2347 | To #2994 |
|---|
| note | The general result `IsCyclic Rˣ` for finite integral domains (`isCyclic_of_subgroup_isDomain` and the `instance [Finite Rˣ] : IsCyclic Rˣ`) covers finite fields. | The general result `IsCyclic Rˣ` for finite integral domains (`isCyclic_of_subgroup_isDomain`) covers finite fields. |
modifiedUniqueness up to isomorphism via splitting fieldsd81bf196db30
| Field | From #2347 | To #2994 |
|---|
| note | `GaloisField.algEquivGaloisField` (with `FiniteField.algEquivOfCardEq`) realizes this via the universal property of the splitting field. | `GaloisField.algEquivGaloisField` (with `FiniteField.algEquivOfCardEq`) realizes uniqueness via the universal property of the splitting field. |
modifiedPowers of Frobenius and order n72bc87bc95f0
| Field | From #2347 | To #2994 |
|---|
| note | `FiniteField.frobenius_pow` shows that `frobenius K p ^ n = 1` when `q = p^n`; `FiniteField.orderOf_frobeniusAlgHom` gives the exact order. | `FiniteField.frobenius_pow` shows `frobenius K p ^ n = 1` when `q = p^n`; `FiniteField.orderOf_frobeniusAlgHom` gives the exact order. |
modifiedGF(p^n) is a Galois extension of GF(p) with cyclic Galois group5ac4bec4d11a
| Field | From #2347 | To #2994 |
|---|
| note | `GaloisField.instIsGaloisOfFinite` provides an `IsGalois K K'` instance for any finite extension between finite fields, and the cyclic-Galois-group instance for finite extensions of finite fields supplies cyclicity. | `GaloisField.instIsGaloisOfFinite` provides an `IsGalois K K'` instance for any finite extension between finite fields, and the cyclic-Galois-group instance supplies cyclicity. |
modifiedUnique factorization of monic polynomials over finite fieldsa58ca5c10f80
| Field | From #2347 | To #2994 |
|---|
| note | Polynomial rings over UFDs are UFDs by the global instance in `Mathlib/RingTheory/Polynomial/UniqueFactorization.lean`, which applies to fields. | Polynomial rings over UFDs are UFDs via the global instance `Polynomial.uniqueFactorizationMonoid`, which applies to fields. |
modifiedExistence of irreducible polynomial of every degree999681673588
| Field | From #2347 | To #2994 |
|---|
| note | Existence follows abstractly because `GaloisField p n` exists with degree `n` over `ZMod p`, but no direct theorem of the form `∃ f : (ZMod p)[X], Irreducible f ∧ degree f = n` is isolated. | Existence follows abstractly because `GaloisField p n` exists with degree `n` over `ZMod p`, but no direct `∃ f : (ZMod p)[X], Irreducible f ∧ degree f = n` is isolated. |
addedCharacteristic of a finite field is prime2e8c6dc1c153
addedFinite field is a vector space over its prime subfield8c0f68d38578