Galois

📁 Source: Mathlib/NumberTheory/RamificationInertia/Galois.lean

Statistics

Metric	Count
Definitions inertiaDegIn, instMulActionAlgEquivElemPrimesOver, instMulActionElemPrimesOver, ramificationIdxIn	4
Theorems card_inertia_eq_ramificationIdxIn, card_stabilizer_eq, card_stabilizer_eq_card_inertia_mul_finrank, coe_smul_primesOver, coe_smul_primesOver_eq_map_galRestrict, coe_smul_primesOver_mk, coe_smul_primesOver_mk_eq_map_galRestrict, exists_comap_galRestrict_eq, exists_map_eq_of_isGalois, exists_smul_eq_of_isGaloisGroup, inertiaDegIn_eq_inertiaDeg, inertiaDegIn_mul_inertiaDegIn, inertiaDegIn_ne_zero, inertiaDeg_eq_of_isGalois, inertiaDeg_eq_of_isGaloisGroup, isPretransitive_of_isGalois, isPretransitive_of_isGaloisGroup, ncard_primesOver_mul_card_inertia_mul_finrank, ncard_primesOver_mul_ncard_primesOver, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, ramificationIdxIn_eq_ramificationIdx, ramificationIdxIn_mul_ramificationIdxIn, ramificationIdxIn_ne_zero, ramificationIdx_eq_of_isGalois, ramificationIdx_eq_of_isGaloisGroup	25
Total	29

Ideal

Definitions

Name	Category	Theorems
inertiaDegIn 📖	CompOp	9 math math: IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, card_stabilizer_eq, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, inertiaDegIn_mul_inertiaDegIn, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, IsCyclotomicExtension.Rat.inertiaDegIn_eq, inertiaDegIn_eq_inertiaDeg, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime
instMulActionAlgEquivElemPrimesOver 📖	CompOp	2 math math: coe_smul_primesOver_mk_eq_map_galRestrict, coe_smul_primesOver_eq_map_galRestrict
instMulActionElemPrimesOver 📖	CompOp	4 math math: isPretransitive_of_isGalois, coe_smul_primesOver_mk, isPretransitive_of_isGaloisGroup, coe_smul_primesOver
ramificationIdxIn 📖	CompOp	11 math math: IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, card_stabilizer_eq, ramificationIdxIn_mul_ramificationIdxIn, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, ramificationIdxIn_eq_ramificationIdx, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, card_inertia_eq_ramificationIdxIn, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_inertia_eq_ramificationIdxIn 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike inertia CommRing.toRing DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MulSemiringAction.toDistribMulAction ramificationIdxIn	—	IsPrime.isMaximal IsDedekindDomainDvr.ring_dimensionLEOne IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr IsPrime.under IsMaximal.isPrime' over_def ncard_primesOver_mul_card_inertia_mul_finrank mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero primesOver_ncard_ne_zero Algebra.IsIntegral.of_finite mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero MulZeroClass.mul_zero One.instNonempty Finite.not_infinite mul_assoc inertiaDeg_algebraMap inertiaDegIn_eq_inertiaDeg ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn
card_stabilizer_eq 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction ramificationIdxIn inertiaDegIn	—	IsPrime.isMaximal IsDedekindDomainDvr.ring_dimensionLEOne IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr IsPrime.under IsMaximal.isPrime' over_def card_stabilizer_eq_card_inertia_mul_finrank card_inertia_eq_ramificationIdxIn inertiaDegIn_eq_inertiaDeg inertiaDeg_algebraMap
card_stabilizer_eq_card_inertia_mul_finrank 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule pointwiseDistribMulAction inertia CommRing.toRing NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Module.finrank HasQuotient.Quotient instHasQuotient_1 Quotient.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing Algebra.toModule Quotient.commSemiring Quotient.algebraOfLiesOver	—	Quotient.normal IsGaloisGroup.isInvariant Quotient.finite_of_isInvariant IsGaloisGroup.commutes Nat.card_congr instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia IsMaximal.isPrime' IsGalois.card_aut_eq_finrank Subgroup.card_mul_index inertia_le_stabilizer
coe_smul_primesOver 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemPrimesOver SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	—
coe_smul_primesOver_eq_map_galRestrict 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MulAction.toSemigroupAction instMulActionAlgEquivElemPrimesOver map AlgEquiv.instFunLike DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike galRestrict Algebra.IsAlgebraic.of_finite EuclideanDomain.toCommRing Field.toEuclideanDomain IsLocalRing.toNontrivial Field.instIsLocalRing DivisionRing.toRing Field.toDivisionRing	—	—
coe_smul_primesOver_mk 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemPrimesOver SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	—
coe_smul_primesOver_mk_eq_map_galRestrict 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MulAction.toSemigroupAction instMulActionAlgEquivElemPrimesOver map AlgEquiv.instFunLike DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike galRestrict Algebra.IsAlgebraic.of_finite EuclideanDomain.toCommRing Field.toEuclideanDomain IsLocalRing.toNontrivial Field.instIsLocalRing DivisionRing.toRing Field.toDivisionRing	—	—
exists_comap_galRestrict_eq 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver	comap AlgEquiv AlgEquiv.instFunLike DFunLike.coe MulEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike galRestrict Algebra.IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable AlgHomClass.toRingHomClass AlgEquiv.instEquivLike AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass	—	MulEquiv.isDomain instIsDomainSubtypeMemSubalgebraIntegralClosure instIsDomain integralClosure.isIntegralClosure IsScalarTower.subalgebra' IsScalarTower.right IsIntegralClosure.isDedekindDomain IsDedekindDomain.toIsDomain IsGalois.to_isSeparable IsIntegralClosure.finite IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsDedekindDomainDvr.toIsNoetherian IsIntegralClosure.isFractionRing_of_finite_extension Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsGaloisGroup.of_isFractionRing instSMulDistribClassAlgEquiv IsGaloisGroup.of_isGalois Algebra.IsIntegral.of_finite AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass exists_smul_eq_of_isGaloisGroup Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors comap_map_of_bijective AlgEquiv.bijective
exists_map_eq_of_isGalois 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction	—	exists_smul_eq_of_isGaloisGroup
exists_smul_eq_of_isGaloisGroup 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid pointwiseDistribMulAction	—	Algebra.IsInvariant.exists_smul_of_under_eq IsGaloisGroup.isInvariant IsGaloisGroup.commutes over_def
inertiaDegIn_eq_inertiaDeg 📖	mathematical	—	inertiaDegIn inertiaDeg	—	inertiaDegIn.eq_1 inertiaDeg_eq_of_isGaloisGroup
inertiaDegIn_mul_inertiaDegIn 📖	mathematical	—	inertiaDegIn	—	nonempty_primesOver IsDomain.toNontrivial Algebra.IsIntegral.of_finite LiesOver.trans inertiaDegIn_eq_inertiaDeg inertiaDeg_algebra_tower
inertiaDegIn_ne_zero 📖	—	—	—	—	nonempty_primesOver Algebra.IsIntegral.of_finite IsMaximal.isPrime' inertiaDegIn_eq_inertiaDeg primesOver.isPrime primesOver.liesOver inertiaDeg_ne_zero
inertiaDeg_eq_of_isGalois 📖	mathematical	—	inertiaDeg	—	inertiaDeg_eq_of_isGaloisGroup
inertiaDeg_eq_of_isGaloisGroup 📖	mathematical	—	inertiaDeg	—	exists_smul_eq_of_isGaloisGroup IsGaloisGroup.commutes inertiaDeg_map_eq AlgEquiv.instAlgEquivClass
isPretransitive_of_isGalois 📖	mathematical	—	MulAction.IsPretransitive Set.Elem Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemPrimesOver IsGaloisGroup.commutes Ring.toSemiring CommRing.toRing	—	isPretransitive_of_isGaloisGroup
isPretransitive_of_isGaloisGroup 📖	mathematical	—	MulAction.IsPretransitive Set.Elem Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemPrimesOver IsGaloisGroup.commutes Ring.toSemiring CommRing.toRing	—	IsGaloisGroup.commutes exists_smul_eq_of_isGaloisGroup
ncard_primesOver_mul_card_inertia_mul_finrank 📖	mathematical	—	Set.ncard Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike inertia CommRing.toRing DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Module.finrank HasQuotient.Quotient instHasQuotient_1 Quotient.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Quotient.commRing Algebra.toModule Quotient.commSemiring Quotient.algebraOfLiesOver	—	mul_assoc card_stabilizer_eq_card_inertia_mul_finrank Algebra.IsInvariant.orbit_eq_primesOver IsGaloisGroup.isInvariant IsGaloisGroup.commutes IsMaximal.isPrime' Nat.card_prod Nat.card_congr
ncard_primesOver_mul_ncard_primesOver 📖	mathematical	—	Set.ncard Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver	—	ne_bot_of_liesOver_of_ne_bot IsDedekindDomain.toIsDomain IsDomain.toNontrivial mul_ne_zero IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd ramificationIdxIn_ne_zero IsMaximal.isPrime' inertiaDegIn_ne_zero ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn inertiaDegIn_mul_inertiaDegIn ramificationIdxIn_mul_ramificationIdxIn map_ne_bot_of_ne_bot Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsGaloisGroup.card_eq_finrank IsGaloisGroup.toFractionRing Module.finrank_mul_finrank FractionRing.instIsScalarTower_1 FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower commRing_strongRankCondition FractionRing.instNontrivial Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule IsDomain.to_noZeroDivisors instIsDomain instFiniteDimensionalFractionRingOfFinite instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 📖	mathematical	—	Set.ncard Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver ramificationIdxIn inertiaDegIn Nat.card	—	IsDedekindDomain.toIsDomain smul_eq_mul coe_primesOverFinset Set.ncard_coe_finset Finset.sum_const FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial IsGaloisGroup.card_eq_finrank IsGaloisGroup.toFractionRing sum_ramification_inertia Localization.isLocalization OreLocalization.instIsScalarTower IsScalarTower.right FractionRing.instIsScalarTower IsScalarTower.left Finset.sum_congr Finset.mem_coe ramificationIdxIn_eq_ramificationIdx inertiaDegIn_eq_inertiaDeg
ramificationIdxIn_eq_ramificationIdx 📖	mathematical	—	ramificationIdxIn ramificationIdx algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	ramificationIdxIn.eq_1 ramificationIdx_eq_of_isGaloisGroup
ramificationIdxIn_mul_ramificationIdxIn 📖	mathematical	—	ramificationIdxIn	—	nonempty_primesOver IsDomain.toNontrivial Algebra.IsIntegral.of_finite LiesOver.trans ramificationIdxIn_eq_ramificationIdx ramificationIdx_algebra_tower map_comap_le over_def
ramificationIdxIn_ne_zero 📖	—	—	—	—	Algebra.IsInvariant.isIntegral IsGaloisGroup.isInvariant nonempty_primesOver IsDomain.toNontrivial IsDedekindDomain.toIsDomain ramificationIdxIn_eq_ramificationIdx primesOver.isPrime primesOver.liesOver IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver
ramificationIdx_eq_of_isGalois 📖	mathematical	—	ramificationIdx algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	ramificationIdx_eq_of_isGaloisGroup
ramificationIdx_eq_of_isGaloisGroup 📖	mathematical	—	ramificationIdx algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	exists_smul_eq_of_isGaloisGroup IsGaloisGroup.commutes ramificationIdx_map_eq AlgEquiv.instAlgEquivClass

---

← Back to Index