Galois fields #
If p
is a prime number, and n
a natural number,
then GaloisField p n
is defined as the splitting field of X^(p^n) - X
over ZMod p
.
It is a finite field with p ^ n
elements.
Main definition #
GaloisField p n
is a field withp ^ n
elements
Main Results #
GaloisField.algEquivGaloisField
: Any finite field is isomorphic to some Galois fieldFiniteField.algEquivOfCardEq
: Uniqueness of finite fields : algebra isomorphismFiniteField.ringEquivOfCardEq
: Uniqueness of finite fields : ring isomorphism
instance
FiniteField.isSplittingField_sub
(K : Type u_1)
(F : Type u_2)
[Field K]
[Fintype K]
[Field F]
[Algebra F K]
:
Polynomial.IsSplittingField F K (Polynomial.X ^ Fintype.card K - Polynomial.X)
A finite field with p ^ n
elements.
Every field with the same cardinality is (non-canonically)
isomorphic to this field.
Equations
- GaloisField p n = Polynomial.SplittingField (Polynomial.X ^ p ^ n - Polynomial.X)
Instances For
Equations
- instFieldGaloisField p n = inferInstanceAs (Field (Polynomial.SplittingField (Polynomial.X ^ p ^ n - Polynomial.X)))
Equations
- instInhabitedGaloisFieldOfNatNatInstOfNatNatMkPrimePrime_two = { default := 37 }
instance
GaloisField.instAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldZModToSemiringToDivisionSemiringInstFieldGaloisField
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
:
Algebra (ZMod p) (GaloisField p n)
Equations
- One or more equations did not get rendered due to their size.
instance
GaloisField.instIsSplittingFieldZModGaloisFieldInstFieldZModInstFieldGaloisFieldInstAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldZModToSemiringToDivisionSemiringInstFieldGaloisFieldHSubPolynomialPolynomialPolynomialToSemiringToDivisionSemiringToSemifieldHPowNatInstHPowPowToMonoidToMonoidWithZeroSemiringXHPowInstHPowInstPowNatX
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
:
Polynomial.IsSplittingField (ZMod p) (GaloisField p n) (Polynomial.X ^ p ^ n - Polynomial.X)
Equations
- One or more equations did not get rendered due to their size.
instance
GaloisField.instCharPGaloisFieldToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingInstFieldGaloisField
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
:
CharP (GaloisField p n) p
Equations
- One or more equations did not get rendered due to their size.
instance
GaloisField.instFiniteDimensionalZModGaloisFieldToDivisionRingInstFieldZModToAddCommGroupToRingInstFieldGaloisFieldToModuleToCommSemiringToSemifieldToSemiringToDivisionSemiringInstAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldZModToSemiringToDivisionSemiringInstFieldGaloisField
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
:
FiniteDimensional (ZMod p) (GaloisField p n)
Equations
- One or more equations did not get rendered due to their size.
instance
GaloisField.instFintypeGaloisField
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
:
Fintype (GaloisField p n)
Equations
theorem
GaloisField.finrank
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
{n : ℕ}
(h : n ≠ 0)
:
FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
theorem
GaloisField.card
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
(h : n ≠ 0)
:
Fintype.card (GaloisField p n) = p ^ n
theorem
GaloisField.splits_zmod_X_pow_sub_X
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
:
Polynomial.Splits (RingHom.id (ZMod p)) (Polynomial.X ^ p - Polynomial.X)
theorem
GaloisField.splits_X_pow_card_sub_X
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
{K : Type u_1}
[Field K]
[Fintype K]
[Algebra (ZMod p) K]
:
Polynomial.Splits (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)
def
GaloisField.algEquivGaloisField
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
(n : ℕ)
{K : Type u_1}
[Field K]
[Fintype K]
[Algebra (ZMod p) K]
(h : Fintype.card K = p ^ n)
:
K ≃ₐ[ZMod p] GaloisField p n
Any finite field is (possibly non canonically) isomorphic to some Galois field.
Equations
- GaloisField.algEquivGaloisField p n h = Polynomial.IsSplittingField.algEquiv K (Polynomial.X ^ p ^ n - Polynomial.X)
Instances For
def
FiniteField.algEquivOfCardEq
{K : Type u_1}
[Field K]
[Fintype K]
{K' : Type u_2}
[Field K']
[Fintype K']
(p : ℕ)
[h_prime : Fact (Nat.Prime p)]
[Algebra (ZMod p) K]
[Algebra (ZMod p) K']
(hKK' : Fintype.card K = Fintype.card K')
:
Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly non canonically) isomorphic
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
FiniteField.ringEquivOfCardEq
{K : Type u_1}
[Field K]
[Fintype K]
{K' : Type u_2}
[Field K']
[Fintype K']
(hKK' : Fintype.card K = Fintype.card K')
:
K ≃+* K'
Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly non canonically) isomorphic
Equations
- One or more equations did not get rendered due to their size.