Commit 2024-11-12 21:38 20b3d7ac

View on Github →

refactor(FieldTheory/Finite/GaloisField): replace Fintype.card with Nat.card in theorems about GaloisField (#18106) Replace Fintype.card with Nat.card in theorems about GaloisField because we deprecate FiniteDimensional.fintypeOfFintype and GaloisField.instFintype, which are noncomputable def/instance of Fintype. See discussions at Zulip.

Estimated changes

Modified Mathlib/FieldTheory/Cardinality.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

added theorem FiniteField.isSplittingField_of_card_eq

added theorem FiniteField.isSplittingField_of_nat_card_eq

added theorem FiniteField.splits_X_pow_card_sub_X

added theorem FiniteField.splits_X_pow_nat_card_sub_X

modified def GaloisField.algEquivGaloisField

added def GaloisField.algEquivGaloisFieldOfFintype

modified theorem GaloisField.card

deleted theorem GaloisField.isSplittingField_of_card_eq

deleted theorem GaloisField.splits_X_pow_card_sub_X

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/RingTheory/Finiteness.lean