Documentation Verification Report

Gal

📁 Source: Mathlib/NumberTheory/Cyclotomic/Gal.lean

Statistics

Metric	Count
Definitions `autEquivPow`, `fromZetaAut`, `Gal`, `galCyclotomicEquivUnitsZMod`, `galXPowEquivUnitsZMod`	5
Theorems `autEquivPow_apply`, `autEquivPow_symm_apply`, `fromZetaAut_spec`, `autToPow_injective`	4
Total	9

IsCyclotomicExtension

Definitions

Name	Category	Theorems
`autEquivPow` 📖	CompOp	2 math math: `autEquivPow_symm_apply`, `autEquivPow_apply`
`fromZetaAut` 📖	CompOp	1 math math: `fromZetaAut_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`autEquivPow_apply` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MulEquiv` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `ZMod` `ZMod.commRing` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `autEquivPow` `OneHom.toFun` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulOne.toOne` `Units.instMulOneClass` `MonoidHom.toOneHom` `IsPrimitiveRoot.autToPow` `zeta`	—	—
`autEquivPow_symm_apply` 📖	mathematical	`Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `MulEquiv` `Units` `ZMod` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `autEquivPow` `PowerBasis.equivOfMinpoly` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsPrimitiveRoot.powerBasis` `zeta` `Monoid.toNatPow` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `ZMod.val` `Units.val`	—	—
`fromZetaAut_spec` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgEquiv.instFunLike` `fromZetaAut` `zeta` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`IsPrimitiveRoot.powerBasis_gen` `PowerBasis.equivOfMinpoly_gen` `ZMod.val_cast_of_lt`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`autToPow_injective` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`AlgEquiv` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ZMod.commRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMulOneClass` `MonoidHom.instFunLike` `autToPow`	—	`rootsOfUnity.coe_pow` `pow_eq_pow_iff_modEq` `eq_orderOf` `val_toRootsOfUnity_coe` `orderOf_units` `Subgroup.orderOf_coe` `ZMod.natCast_eq_natCast_iff` `AlgEquiv.coe_algHom_injective` `PowerBasis.algHom_ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_rootsOfUnity_eq_pow_self` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass`

Polynomial

Definitions

Name	Category	Theorems
`Gal` 📖	CompOp	30 math math: `Gal.galActionHom_restrict`, `Gal.galActionHom_bijective_of_prime_degree'`, `Gal.smul_def`, `Gal.restrict_smul`, `Gal.galActionHom_injective`, `gal_X_pow_isSolvable`, `Gal.restrictDvd_def`, `solvableByRad.isSolvable'`, `gal_X_pow_sub_C_isSolvable`, `solvableByRad.isSolvable`, `gal_X_pow_sub_C_isSolvable_aux`, `Gal.prime_degree_dvd_card`, `gal_X_pow_sub_one_isSolvable`, `Gal.restrictComp_surjective`, `gal_C_isSolvable`, `gal_X_sub_C_isSolvable`, `gal_one_isSolvable`, `Gal.galAction_isPretransitive`, `Gal.restrict_surjective`, `gal_mul_isSolvable`, `Gal.galActionHom_bijective_of_prime_degree`, `Gal.ext_iff`, `gal_zero_isSolvable`, `Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv`, `gal_isSolvable_of_splits`, `Gal.restrictProd_injective`, `Gal.card_of_separable`, `Gal.restrictDvd_surjective`, `gal_X_isSolvable`, `gal_isSolvable_tower`

(root)

Definitions

Name	Category	Theorems
`galCyclotomicEquivUnitsZMod` 📖	CompOp	—
`galXPowEquivUnitsZMod` 📖	CompOp	—

---

← Back to Index