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`, `card_algEquiv_extension`, `finrank_extension`, `finrank_zmod_extension`, `instFiniteExtension_1`, `instIsScalarTowerZModExtension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `natCard_algEquiv_extension`, `natCard_extension`, `nonempty_algHom_extension`	11
Total	18

FiniteField

Definitions

Name	Category	Theorems
`algEquivExtension` 📖	CompOp	—
`instAlgebraExtension` 📖	CompOp	8 math math: `Extension.frob_apply`, `card_algEquiv_extension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `instIsScalarTowerZModExtension`, `instFiniteExtension_1`, `Extension.exists_frob_pow_eq`, `natCard_algEquiv_extension`, `finrank_extension`
`instAlgebraZModExtension` 📖	CompOp	3 math math: `instIsScalarTowerZModExtension`, `finrank_zmod_extension`, `nonempty_algHom_extension`
`instFieldExtension` 📖	CompOp	10 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`
`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`
`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` `GaloisField` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `ZMod.algebra` `DivisionRing.toRing` `Field.toDivisionRing` `instFieldGaloisField` `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.toNatPow` `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.toNatPow` `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	2 math math: `frob_apply`, `exists_frob_pow_eq`

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.toNatPow` `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.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.card`	—	—

---

← Back to Index