Documentation Verification Report

Galois

📁 Source: Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

Statistics

Metric	Count
Definitions `galEquivZMod`	1
Theorems `galEquivZMod_apply_of_pow_eq`, `galEquivZMod_restrictNormal_apply`, `galEquivZMod_smul_of_pow_eq`	3
Total	4

IsCyclotomicExtension.Rat

Definitions

Name	Category	Theorems
`galEquivZMod` 📖	CompOp	3 math math: `galEquivZMod_apply_of_pow_eq`, `galEquivZMod_restrictNormal_apply`, `galEquivZMod_smul_of_pow_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`galEquivZMod_apply_of_pow_eq` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgEquiv` `Rat.commSemiring` `DivisionRing.toRatAlgebra` `NumberField.to_charZero` `AlgEquiv.instFunLike` `ZMod.val` `Units.val` `ZMod` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MulEquiv` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `galEquivZMod`	—	`NumberField.to_charZero` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `instIsDomain` `IsCyclotomicExtension.zeta_spec` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `pow_right_comm` `galEquivZMod.eq_1` `IsCyclotomicExtension.autEquivPow_apply` `OneHom.toFun_eq_coe` `MonoidHom.toOneHom_coe` `IsPrimitiveRoot.autToPow_spec`
`galEquivZMod_restrictNormal_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `AlgEquiv` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `galEquivZMod` `AlgEquiv.restrictNormal` `Rat.instField` `IsScalarTower.rat` `DivisionRing.toRing` `Ring.toAddCommGroup` `Algebra.toModule` `Semifield.toCommSemiring` `IsGalois.to_normal` `MonoidHom` `Units.instMulOneClass` `MonoidHom.instFunLike` `ZMod.unitsMap`	—	`NumberField.to_charZero` `IsCyclotomicExtension.zeta_spec` `IsScalarTower.rat` `IsGalois.to_normal` `FaithfulSMul.algebraMap_injective` `instFaithfulSMul_1` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `galEquivZMod_apply_of_pow_eq` `IsPrimitiveRoot.pow_eq_one_iff_dvd` `map_one` `MonoidHomClass.toOneHomClass` `AlgEquiv.restrictNormal_commutes` `IsPrimitiveRoot.pow_eq_one` `Units.ext_iff` `ZMod.cast_id` `ZMod.natCast_val` `ZMod.natCast_eq_natCast_iff'` `IsPrimitiveRoot.eq_orderOf` `IsOfFinOrder.pow_inj_mod` `IsPrimitiveRoot.isOfFinOrder`
`galEquivZMod_smul_of_pow_eq` 📖	mathematical	`NumberField.RingOfIntegers` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`AlgEquiv` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `MulSemiringAction.toDistribMulAction` `NumberField.RingOfIntegers.instMulSemiringAction` `AlgEquiv.applyMulSemiringAction` `ZMod.val` `Units.val` `ZMod` `ZMod.commRing` `DFunLike.coe` `MulEquiv` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `galEquivZMod`	—	`NumberField.to_charZero` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NumberField.RingOfIntegers.instIsTorsionFree_2` `galEquivZMod_apply_of_pow_eq` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `Subalgebra.coe_pow` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `OneMemClass.coe_one`

---

← Back to Index