Documentation Verification Report

Extension

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

Statistics

Metric	Count
Definitions `frob`, `algEquivExtension`, `instAlgebraExtension`, `instAlgebraZModExtension`, `instFieldExtension`, `instFiniteDimensionalZModExtension`, `instFiniteExtension`	7
Theorems `exists_frob_pow_eq`, `frob_apply`, `frob_iterate_apply`, `card_algEquiv_extension`, `exists_forall_apply_eq_pow`, `finrank_extension`, `finrank_zmod_extension`, `instFiniteExtension_1`, `instIsScalarTowerZModExtension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `natCard_algEquiv_extension`, `natCard_extension`, `nonempty_algHom_extension`, `natDegree_dvd_of_dvd_X_pow_card_pow_sub_X`	14
Total	21

FiniteField

Definitions

Name	Category	Theorems
`algEquivExtension` 📖	CompOp	—
`instAlgebraExtension` 📖	CompOp	9 math math: `Extension.frob_apply`, `card_algEquiv_extension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `instIsScalarTowerZModExtension`, `instFiniteExtension_1`, `Extension.exists_frob_pow_eq`, `natCard_algEquiv_extension`, `finrank_extension`, `Extension.frob_iterate_apply`
`instAlgebraZModExtension` 📖	CompOp	3 math math: `instIsScalarTowerZModExtension`, `finrank_zmod_extension`, `nonempty_algHom_extension`
`instFieldExtension` 📖	CompOp	11 math math: `Extension.frob_apply`, `card_algEquiv_extension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `instIsScalarTowerZModExtension`, `finrank_zmod_extension`, `instFiniteExtension_1`, `nonempty_algHom_extension`, `Extension.exists_frob_pow_eq`, `natCard_algEquiv_extension`, `finrank_extension`, `Extension.frob_iterate_apply`
`instFiniteDimensionalZModExtension` 📖	CompOp	—
`instFiniteExtension` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_algEquiv_extension` 📖	mathematical	—	`Fintype.card` `AlgEquiv` `Extension` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instFieldExtension` `instAlgebraExtension` `AlgEquiv.fintype` `instFiniteExtension_1`	—	`instFiniteExtension_1` `Fintype.card_eq_nat_card` `natCard_algEquiv_extension`
`exists_forall_apply_eq_pow` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `Nat.card`	—	`NeZero.of_pos` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `isNoetherian_of_finite` `Module.Projective.of_free` `Module.Free.of_divisionRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Extension.exists_frob_pow_eq` `AlgEquiv.symm_apply_apply` `Extension.frob_iterate_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.congr_arg` `AlgEquiv.congr_fun`
`finrank_extension` 📖	mathematical	—	`Module.finrank` `Extension` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instFieldExtension` `Algebra.toModule` `Semifield.toCommSemiring` `instAlgebraExtension`	—	`Nat.pow_right_injective` `Finite.one_lt_card` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instFiniteExtension_1` `natCard_extension`
`finrank_zmod_extension` 📖	mathematical	—	`Module.finrank` `ZMod` `Extension` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ZMod.instField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instFieldExtension` `Algebra.toModule` `Semifield.toCommSemiring` `instAlgebraZModExtension`	—	`ZMod.instSubsingletonAlgebra` `GaloisField.finrank` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `ZMod.nontrivial` `Nat.Prime.one_lt'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `isNoetherian_of_finite` `Module.Projective.of_free` `Module.Free.of_divisionRing` `ZMod.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instFiniteExtension_1` 📖	mathematical	—	`Module.Finite` `Extension` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instFieldExtension` `Algebra.toModule` `Semifield.toCommSemiring` `instAlgebraExtension`	—	`Module.Finite.of_finite`
`instIsScalarTowerZModExtension` 📖	mathematical	—	`IsScalarTower` `ZMod` `Extension` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `ZMod.instField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instFieldExtension` `instAlgebraExtension` `instAlgebraZModExtension`	—	`IsScalarTower.of_algebraMap_eq'` `ZMod.subsingleton_ringHom`
`instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard` 📖	mathematical	—	`Polynomial.IsSplittingField` `Extension` `instFieldExtension` `instAlgebraExtension` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Nat.instMonoid` `Nat.card`	—	`Fintype.card_eq_nat_card` `natCard_extension` `isSplittingField_sub`
`natCard_algEquiv_extension` 📖	mathematical	—	`Nat.card` `AlgEquiv` `Extension` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instFieldExtension` `instAlgebraExtension`	—	`IsGalois.card_aut_eq_finrank` `instFiniteExtension_1` `GaloisField.instIsGaloisOfFinite` `finrank_extension`
`natCard_extension` 📖	mathematical	—	`Nat.card` `Extension` `Monoid.toPow` `Nat.instMonoid`	—	`pow_finrank_eq_natCard` `finrank_zmod_extension` `pow_mul`
`nonempty_algHom_extension` 📖	mathematical	—	`AlgHom` `ZMod` `Extension` `Semifield.toCommSemiring` `Field.toSemifield` `ZMod.instField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instFieldExtension` `instAlgebraZModExtension`	—	`nonempty_algHom_of_finrank_dvd` `dvd_mul_right` `finrank_zmod_extension`

FiniteField.Extension

Definitions

Name	Category	Theorems
`frob` 📖	CompOp	3 math math: `frob_apply`, `exists_frob_pow_eq`, `frob_iterate_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_frob_pow_eq` 📖	mathematical	—	`AlgEquiv` `FiniteField.Extension` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FiniteField.instFieldExtension` `FiniteField.instAlgebraExtension` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `frob`	—	`Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `isNoetherian_of_finite` `FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow` `FiniteField.finrank_extension` `AlgEquiv.ext` `AlgEquiv.coe_pow`
`frob_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `FiniteField.Extension` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FiniteField.instFieldExtension` `FiniteField.instAlgebraExtension` `AlgEquiv.instFunLike` `frob` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.card`	—	—
`frob_iterate_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `FiniteField.Extension` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FiniteField.instFieldExtension` `FiniteField.instAlgebraExtension` `AlgEquiv.instFunLike` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `frob` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `Nat.card`	—	`pow_zero` `pow_one` `pow_add` `AlgEquiv.mul_apply` `frob_apply` `pow_mul`

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natDegree_dvd_of_dvd_X_pow_card_pow_sub_X` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `Polynomial.X` `Nat.instMonoid` `Nat.card`	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`eq_or_ne` `finite_or_infinite` `CharP.exists` `CharP.char_is_prime` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FiniteField.finrank_extension` `Polynomial.Irreducible.natDegree_dvd_finrank` `Polynomial.Splits.of_dvd` `Polynomial.IsSplittingField.splits` `FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `FiniteField.X_pow_card_pow_sub_X_ne_zero` `Finite.one_lt_card` `Polynomial.map_dvd` `Polynomial.Splits.natDegree_eq_one_of_irreducible` `Polynomial.Splits.X_sub_C` `Polynomial.X_sub_C_ne_zero` `neg_sub` `dvd_neg` `pow_zero` `zero_pow` `Nat.card_eq_zero_of_infinite` `one_dvd`

---

← Back to Index