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, galEquivZMod_stabilizer, mem_zpowers_galEquivZMod_of_mem_stabilizer	5
Total	6

IsCyclotomicExtension.Rat

Definitions

Name	Category	Theorems
galEquivZMod 📖	CompOp	5 math math: mem_zpowers_galEquivZMod_of_mem_stabilizer, galEquivZMod_apply_of_pow_eq, galEquivZMod_restrictNormal_apply, galEquivZMod_stabilizer, galEquivZMod_smul_of_pow_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
galEquivZMod_apply_of_pow_eq 📖	mathematical	Monoid.toPow 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero AlgEquiv.instFunLike Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	AlgEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.RingOfIntegers SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NumberField.instCommRingRingOfIntegers DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MulSemiringAction.toDistribMulAction Ring.toSemiring NumberField.RingOfIntegers.instMulSemiringAction AlgEquiv.applyMulSemiringAction Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring 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 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
galEquivZMod_stabilizer 📖	mathematical	—	DFunLike.coe OrderIso Subgroup AlgEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero AlgEquiv.aut Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder instFunLikeOrderIso MulEquiv.mapSubgroup galEquivZMod MulAction.stabilizer Ideal NumberField.RingOfIntegers NumberField.instCommRingRingOfIntegers DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction NumberField.RingOfIntegers.instMulSemiringAction AlgEquiv.applyMulSemiringAction Subgroup.zpowers ZMod.unitOfCoprime	—	NumberField.to_charZero IsCyclotomicExtension.isGalois SetLike.ext' Set.eq_of_subset_of_card_le mem_zpowers_galEquivZMod_of_mem_stabilizer Nat.Prime.coprime_iff_not_dvd Fact.out Fintype.card_eq_nat_card SetLike.coe_sort_coe Nat.card_zpowers MulEquiv.mapSubgroup_apply Subgroup.coe_map Nat.card_image_equiv Ideal.card_stabilizer_eq instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain NumberField.RingOfIntegers.instIsDedekindDomain AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg NumberField.RingOfIntegers.instFG instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 IsDomain.toIsCancelMulZero Nat.Prime.ne_zero Algebra.IsAlgebraic.isSeparable_of_perfectField Int.ideal_span_isMaximal_of_prime Normal.toIsAlgebraic IsGalois.to_normal GaloisField.instIsGaloisOfFinite instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal PerfectField.ofFinite Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' inertiaDegIn_eq_of_not_dvd ramificationIdxIn_eq_of_not_dvd one_mul orderOf_injective Units.coeHom_injective Units.coeHom_apply ZMod.coe_unitOfCoprime le_refl
mem_zpowers_galEquivZMod_of_mem_stabilizer 📖	mathematical	AlgEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero Subgroup AlgEquiv.aut SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction NumberField.RingOfIntegers.instMulSemiringAction AlgEquiv.applyMulSemiringAction	Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers ZMod.unitOfCoprime DFunLike.coe MulEquiv AlgEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike galEquivZMod	—	NumberField.to_charZero IsCyclotomicExtension.zeta_spec Int.ideal_span_isMaximal_of_prime AddGroup.int_smulCommClass' IsScalarTower.right IsScalarTower.left instIsFractionRing ringChar.of_eq Int.ringChar_idealQuot Ring.HasFiniteQuotients.finiteQuotient Ring.HasFiniteQuotients.instOfIsDomainOfFG NumberField.RingOfIntegers.instFG NumberField.RingOfIntegers.instNeZeroIdealOfIsMaximal FiniteField.exists_forall_apply_eq_pow Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.instIsTwoSided_1 IsPrimitiveRoot.toInteger_isPrimitiveRoot NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Ideal.IsMaximal.ne_top IsDomain.toNontrivial IsDedekindDomain.toIsDomain Ideal.absNorm_eq_pow_inertiaDeg' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg Fact.out Units.ext_iff ZMod.natCast_zmod_val Units.val_pow_eq_pow_val ZMod.coe_unitOfCoprime Nat.cast_pow ZMod.natCast_eq_natCast_iff' IsPrimitiveRoot.eq_orderOf IsOfFinOrder.pow_inj_mod IsPrimitiveRoot.isOfFinOrder map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass galEquivZMod_smul_of_pow_eq IsPrimitiveRoot.pow_eq_one Int.card_ideal_quot RingHomCompTriple.comp_apply RingHomCompTriple.right_ids

---

← Back to Index