GaloisField

📁 Source: Mathlib/FieldTheory/Finite/GaloisField.lean

Statistics

Metric	Count
Definitions algEquivOfCardEq, ringEquivOfCardEq, GaloisField, algEquivGaloisField, algEquivGaloisFieldOfFintype, equivZmodP, instAlgebraZModGaloisField, instCharPGaloisField, instFieldGaloisField, instFiniteDimensionalZModGaloisField, instFiniteGaloisField, instInhabitedGaloisField, instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX	13
Theorems algebraMap_norm_eq_pow, card_algHom_of_finrank_dvd, isSplittingField_of_card_eq, isSplittingField_of_nat_card_eq, isSplittingField_sub, natCard_algHom_of_finrank_dvd, nonempty_algHom_iff_finrank_dvd, nonempty_algHom_of_finrank_dvd, norm_surjective, pow_finrank_eq_card, pow_finrank_eq_natCard, splits_X_pow_card_sub_X, splits_X_pow_nat_card_sub_X, unitsMap_norm_surjective, card, finrank, instIsGaloisOfFinite, splits_zmod_X_pow_sub_X, galois_poly_separable	19
Total	32

FiniteField

Definitions

Name	Category	Theorems
algEquivOfCardEq 📖	CompOp	—
ringEquivOfCardEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_norm_eq_pow 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.card	—	Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Algebra.norm_eq_prod_automorphisms GaloisField.instIsGaloisOfFinite Algebra.IsAlgebraic.of_finite Function.Bijective.prod_comp bijective_frobeniusAlgEquivOfAlgebraic_pow Finset.prod_congr AlgEquiv.coe_pow pow_iterate Finset.prod_pow_eq_pow_sum Fin.sum_univ_eq_sum_range Nat.geomSum_eq Fintype.one_lt_card
card_algHom_of_finrank_dvd 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	Fintype.card AlgHom minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain Module.instFiniteDimensionalOfIsReflexive Ring.toAddCommGroup Ring.toSemiring Module.instIsReflexiveOfFiniteOfProjective AddCommGroup.toAddCommMonoid Module.IsNoetherian.finite CommSemiring.toSemiring isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing	—	instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Fintype.card_eq_nat_card natCard_algHom_of_finrank_dvd
isSplittingField_of_card_eq 📖	mathematical	Fintype.card Monoid.toNatPow Nat.instMonoid	Polynomial.IsSplittingField ZMod ZMod.instField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	isSplittingField_sub
isSplittingField_of_nat_card_eq 📖	mathematical	Nat.card Monoid.toNatPow Nat.instMonoid	Polynomial.IsSplittingField ZMod ZMod.instField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	Nat.card_pos_iff pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.Prime.pos Fact.out Nat.card_eq_fintype_card isSplittingField_sub
isSplittingField_sub 📖	mathematical	—	Polynomial.IsSplittingField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Fintype.card	—	X_pow_card_sub_X_natDegree_eq Fintype.one_lt_card IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain Polynomial.splits_iff_card_roots Polynomial.map_sub Polynomial.map_pow Polynomial.map_X roots_X_pow_card_sub_X Finset.card_def Finset.card_univ Polynomial.roots.congr_simp Finset.val_toFinset Finset.coe_univ Algebra.adjoin_univ
natCard_algHom_of_finrank_dvd 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	Nat.card AlgHom	—	nonempty_algHom_of_finrank_dvd Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Nat.card_congr IsScalarTower.of_algHom IsGalois.to_normal GaloisField.instIsGaloisOfFinite IsGalois.card_aut_eq_finrank Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing
nonempty_algHom_iff_finrank_dvd 📖	mathematical	—	AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	—	Module.finrank_mul_finrank IsScalarTower.of_algHom commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing dvd_mul_right nonempty_algHom_of_finrank_dvd
nonempty_algHom_of_finrank_dvd 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	AlgHom	—	Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.finite_of_finrank_pos commRing_strongRankCondition Module.Free.of_divisionRing Module.finrank_pos Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_finite Module.Projective.of_free instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.finite_of_finite isSplittingField_sub Polynomial.Splits.of_dvd Polynomial.IsSplittingField.splits Polynomial.map_ne_zero X_pow_card_sub_X_ne_zero Fintype.one_lt_card Module.card_eq_pow_finrank Polynomial.map_dvd_map' dvd_pow_pow_sub_self_of_dvd
norm_surjective 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm	—	eq_or_ne Algebra.norm_zero IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free unitsMap_norm_surjective
pow_finrank_eq_card 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid Module.finrank ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField AddCommGroup.toAddCommMonoid Fintype.card	—	pow_finrank_eq_natCard Finite.of_fintype Fintype.card_eq_nat_card
pow_finrank_eq_natCard 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid Module.finrank ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField AddCommGroup.toAddCommMonoid Nat.card	—	Module.natCard_eq_pow_finrank Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Nat.card_zmod
splits_X_pow_card_sub_X 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map ZMod CommSemiring.toSemiring Semifield.toCommSemiring ZMod.instField algebraMap Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Fintype.card	—	Polynomial.IsSplittingField.splits isSplittingField_sub
splits_X_pow_nat_card_sub_X 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map ZMod CommSemiring.toSemiring Semifield.toCommSemiring ZMod.instField algebraMap Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.card	—	Nat.card_eq_fintype_card Polynomial.IsSplittingField.splits isSplittingField_sub
unitsMap_norm_surjective 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map Algebra.norm EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	Finite.of_injective_finite_range RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Subtype.finite MonoidHom.surjective_of_card_ker_le_div instFiniteUnits Nat.card_units Set.ncard_coe_finset SetLike.coe_sort_coe Nat.card_coe_set_eq Set.ext algebraMap_norm_eq_pow map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.filter.congr_simp Finset.coe_filter IsCyclic.card_pow_eq_one_le instIsCyclicUnitsOfFinite instIsDomain Nat.card_le_card_of_injective Finite.one_lt_card

GaloisField

Definitions

Name	Category	Theorems
algEquivGaloisField 📖	CompOp	—
algEquivGaloisFieldOfFintype 📖	CompOp	—
equivZmodP 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Nat.card GaloisField Monoid.toNatPow Nat.instMonoid	—	isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Nat.card_eq_fintype_card NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Module.card_fintype Module.finrank_eq_card_basis commRing_strongRankCondition ZMod.nontrivial ZMod.card finrank
finrank 📖	mathematical	—	Module.finrank ZMod GaloisField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldGaloisField Algebra.toModule Semifield.toCommSemiring instAlgebraZModGaloisField	—	Nat.Prime.one_lt Fact.out FiniteField.X_pow_card_pow_sub_X_ne_zero instIsDomain Polynomial.card_rootSet_eq_natDegree galois_poly_separable ZMod.charP dvd_pow dvd_refl Polynomial.SplittingField.splits FiniteField.X_pow_card_pow_sub_X_natDegree_eq Set.eq_univ_iff_forall Polynomial.SplittingField.adjoin_rootSet Subring.closure_induction Polynomial.mem_rootSet_of_ne ZMod.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X RingHom.instRingHomClass ZMod.pow_card_pow sub_self Polynomial.IsSplittingField.instIsTorsionFreeSplittingField Polynomial.coeff_zero_eq_aeval_zero' Polynomial.coeff_sub Polynomial.coeff_X_pow Polynomial.coeff_X_zero sub_zero IsLocalRing.toNontrivial Field.instIsLocalRing NeZero.one ZMod.nontrivial Nat.Prime.one_lt' eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Polynomial.aeval_sub one_pow Polynomial.aeval_X_pow add_pow_char_pow sub_neg_eq_add neg_pow neg_one_pow_char_pow neg_mul one_mul neg_add_cancel mul_pow Nat.pow_right_injective NeZero.of_gt' ZMod.card Module.card_eq_pow_finrank Fintype.ofEquiv_card Fintype.card_congr'
instIsGaloisOfFinite 📖	mathematical	—	IsGalois	—	nonempty_fintype CharP.exists IsGalois.of_separable_splitting_field FiniteField.isSplittingField_sub galois_poly_separable FiniteField.card charP_of_injective_algebraMap' Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing dvd_pow_self PNat.ne_zero
splits_zmod_X_pow_sub_X 📖	mathematical	—	Polynomial.Splits ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	Nat.Prime.one_lt Fact.out ZMod.instIsDomain NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' instIsDomain ZMod.card FiniteField.roots_X_pow_card_sub_X FiniteField.X_pow_card_sub_X_natDegree_eq Polynomial.splits_iff_card_roots Finset.card_def Finset.card_univ

(root)

Definitions

Name	Category	Theorems
GaloisField 📖	CompOp	3 math math: FiniteField.instIsScalarTowerZModExtension, GaloisField.finrank, GaloisField.card
instAlgebraZModGaloisField 📖	CompOp	1 math math: GaloisField.finrank
instCharPGaloisField 📖	CompOp	—
instFieldGaloisField 📖	CompOp	2 math math: FiniteField.instIsScalarTowerZModExtension, GaloisField.finrank
instFiniteDimensionalZModGaloisField 📖	CompOp	—
instFiniteGaloisField 📖	CompOp	—
instInhabitedGaloisField 📖	CompOp	—
instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
galois_poly_separable 📖	mathematical	—	Polynomial.Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring Polynomial.instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	Polynomial.derivative_sub Polynomial.derivative_X_pow Polynomial.derivative_X Polynomial.C_eq_natCast CharP.cast_eq_zero_iff Polynomial.instCharP Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add

---

← Back to Index