Commit 2023-06-21 14:35 f707e57f

View on Github →

feat: port FieldTheory.Finite.GaloisField (#5139) ~~This PR should wait until the discussion here is resolved~~

depends on: #5284

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Finite/GaloisField.lean

added def FiniteField.algEquivOfCardEq

added def FiniteField.ringEquivOfCardEq

added def GaloisField.algEquivGaloisField

added theorem GaloisField.card

added def GaloisField.equivZmodP

added theorem GaloisField.finrank

added theorem GaloisField.isSplittingField_of_card_eq

added theorem GaloisField.splits_x_pow_card_sub_x

added theorem GaloisField.splits_zMod_x_pow_sub_x

added def GaloisField

added theorem galois_poly_separable