Commit 2025-03-14 03:11 d6338631

View on Github →

feat: Galois groups of finite fields (#22885)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.coe_pow

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem AlgHom.coe_pow

Modified Mathlib/Algebra/CharP/Lemmas.lean

added theorem iterateFrobenius_eq_pow

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow

added theorem FiniteField.bijective_frobeniusAlgHom_pow

modified theorem FiniteField.card'

added theorem FiniteField.coe_frobeniusAlgEquivOfAlgebraic

added theorem FiniteField.coe_frobeniusAlgHom

added def FiniteField.frobeniusAlgHom

added theorem FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic

added theorem FiniteField.orderOf_frobeniusAlgHom

deleted theorem card_eq_pow_finrank

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Finiteness.lean

added theorem Module.card_eq_pow_finrank

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem IsOfFinOrder.pow_eq_pow_iff_modEq

added theorem IsOfFinOrder.pow_inj_mod

deleted def IsOfFinOrder.unit

modified theorem finEquivPowers_apply

modified theorem finEquivPowers_symm_apply

modified theorem finEquivZPowers_apply

modified theorem finEquivZPowers_symm_apply

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.bijective_of_subsingleton

modified theorem Function.injective_of_subsingleton

Modified Mathlib/RingTheory/LittleWedderburn.lean