KummerDedekind

📁 Source: Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

Statistics

Metric	Count
Definitions primesOverSpanEquivMonicFactorsMod, ZModXQuotSpanEquivQuotSpan, ZModXQuotSpanEquivQuotSpanPair, exponent, monicFactorsMod	5
Theorems inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', liesOver_primesOverSpanEquivMonicFactorsMod_symm, primesOverSpanEquivMonicFactorsMod_symm_apply, primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', ZModXQuotSpanEquivQuotSpan_mk_apply, exponent_eq_one_iff, exponent_eq_sInf, not_dvd_exponent_iff	11
Total	16

NumberField.Ideal

Definitions

Name	Category	Theorems
primesOverSpanEquivMonicFactorsMod 📖	CompOp	6 math math: ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, primesOverSpanEquivMonicFactorsMod_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ideal Set.instMembership Ideal.primesOver Int.instCommSemiring Ring.toIntAlgebra CommRing.toRing DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod Polynomial.natDegree	—	liesOver_primesOverSpanEquivMonicFactorsMod_symm primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span Ideal.inertiaDeg_algebraMap Int.ideal_span_isMaximal_of_prime IsScalarTower.right finrank_quotient_span_eq_natDegree Algebra.finrank_eq_of_equiv_equiv Ideal.Quotient.ringHom_ext Ideal.instIsTwoSided_1 RingHom.ext eq_intCast RingHom.instRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ideal Set.instMembership Ideal.primesOver Int.instCommSemiring Ring.toIntAlgebra CommRing.toRing DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod Polynomial.natDegree	—	Polynomial.map_surjective ZMod.ringHom_surjective inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply
liesOver_primesOverSpanEquivMonicFactorsMod_symm 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing	Ideal.LiesOver Int.instCommSemiring NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instInsert AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Set.instSingletonSet DFunLike.coe AlgHom Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span Subtype.prop
primesOverSpanEquivMonicFactorsMod_symm_apply 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod	Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Set Set.instMembership Ideal.primesOver Int.instCommSemiring Ideal.span Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod setOf Multiset Multiset.instMembership UniqueFactorizationMonoid.normalizedFactors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.normalizationMonoid Ideal.uniqueFactorizationMonoid NumberField.RingOfIntegers.instIsDedekindDomain Ideal.map RingHom Semiring.toNonAssocSemiring Int.instCommRing RingHom.instFunLike algebraMap HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.Quotient.semiring Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Polynomial.commSemiring Ideal.Quotient.commSemiring Polynomial.instNormalizationMonoid Ideal.Quotient.commRing Ideal.Quotient.noZeroDivisors Ideal.IsMaximal.isPrime' Ideal.IsMaximal Int.ideal_span_isMaximal_of_prime NormalizedGCDMonoid.toNormalizationMonoid CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero Ideal.Quotient.field PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.commRing Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient Ideal.Quotient.isDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain Polynomial.map minpoly KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk Int.instIsDomain IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain Int.euclideanDomain instIsTorsionFreeIntOfIsAddTorsionFree Ring.toAddCommGroup IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 NumberField.to_charZero IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Codisjoint.eq_top IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Submodule.instOrderTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Ideal.comap RingHom.instRingHomClass conductor Codisjoint Submodule.instPartialOrder RingOfIntegers.not_dvd_exponent_iff NumberField.RingOfIntegers.isIntegral RingHomClass.toRingHom RingEquiv Int.instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Distrib.toAdd RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm Int.quotientSpanNatEquivZMod	—	—
primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing	Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Set Set.instMembership Ideal.primesOver Int.instCommSemiring Ideal.span Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod Set.instInsert AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AlgHom Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Ideal.uniqueFactorizationMonoid NumberField.RingOfIntegers.instIsDedekindDomain Ideal.instIsTwoSided_1 Ideal.Quotient.noZeroDivisors Ideal.IsMaximal.isPrime' Int.ideal_span_isMaximal_of_prime PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd Ideal.Quotient.isDomain EuclideanDomain.to_principal_ideal_domain Int.instIsDomain IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 NumberField.to_charZero IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Codisjoint.eq_top RingHom.instRingHomClass RingOfIntegers.not_dvd_exponent_iff NumberField.RingOfIntegers.isIntegral RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Polynomial.map_map Int.quotientSpanNatEquivZMod_comp_castRingHom KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span Ideal.span_union Ideal.span_eq Ideal.map_span Set.image_singleton map_natCast Ideal.span_insert
ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet Ideal Set.instMembership Ideal.primesOver DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod multiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpoly	—	Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity NumberField.RingOfIntegers.instIsDedekindDomain Ideal.map_ne_bot_of_ne_bot Int.instIsDomain NumberField.RingOfIntegers.instNontrivial instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 NumberField.to_charZero IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.primesOver.isPrime multiplicity_eq_of_emultiplicity_eq emultiplicity_map_eq RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass Ideal.instIsTwoSided_1 Ideal.Quotient.noZeroDivisors Ideal.IsMaximal.isPrime' Int.ideal_span_isMaximal_of_prime PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd Ideal.Quotient.isDomain EuclideanDomain.to_principal_ideal_domain Ideal.uniqueFactorizationMonoid IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain Codisjoint.eq_top RingHom.instRingHomClass RingOfIntegers.not_dvd_exponent_iff NumberField.RingOfIntegers.isIntegral Ideal.mem_primesOver_iff_mem_normalizedFactors Subtype.coe_prop KummerDedekind.emultiplicity_factors_map_eq_emultiplicity RingEquivClass.toRingHomClass Polynomial.map_map Int.quotientSpanNatEquivZMod_comp_castRingHom Equiv.apply_symm_apply
ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' 📖	mathematical	RingOfIntegers.exponent Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Finset Finset.instMembership RingOfIntegers.monicFactorsMod	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet Ideal Set.instMembership Ideal.primesOver DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primesOverSpanEquivMonicFactorsMod multiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing minpoly	—	Polynomial.map_surjective ZMod.ringHom_surjective ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply

RingOfIntegers

Definitions

Name	Category	Theorems
ZModXQuotSpanEquivQuotSpan 📖	CompOp	1 math math: ZModXQuotSpanEquivQuotSpan_mk_apply
ZModXQuotSpanEquivQuotSpanPair 📖	CompOp	—
exponent 📖	CompOp	3 math math: exponent_eq_sInf, not_dvd_exponent_iff, exponent_eq_one_iff
monicFactorsMod 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ZModXQuotSpanEquivQuotSpan_mk_apply 📖	mathematical	exponent	DFunLike.coe RingEquiv HasQuotient.Quotient Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing ZMod.commRing Ideal.span Set Set.instSingletonSet Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing minpoly NumberField.RingOfIntegers Int.instCommRing CommRing.toRing NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ZModXQuotSpanEquivQuotSpan RingHom Ring.toSemiring Polynomial.ring DivisionRing.toRing Field.toDivisionRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AlgHom Int.instCommSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Ideal.instIsTwoSided_1 Int.instIsDomain NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.isIntegral AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass Polynomial.map_map Int.quotientSpanNatEquivZMod_comp_castRingHom IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 NumberField.to_charZero IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Codisjoint.eq_top RingHom.instRingHomClass not_dvd_exponent_iff Ideal.map_span Set.image_congr eq_intCast Set.image_singleton Int.cast_natCast KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
exponent_eq_one_iff 📖	mathematical	—	exponent Algebra.adjoin NumberField.RingOfIntegers Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Int.instNontrivial exponent.eq_1 Ideal.absNorm_eq_one_iff Ideal.comap_eq_top_iff conductor_eq_top_iff_adjoin_eq_top
exponent_eq_sInf 📖	mathematical	—	exponent InfSet.sInf Nat.instInfSet setOf NumberField.RingOfIntegers Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule conductor Int.instCommRing Ring.toIntAlgebra CommRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Int.instNontrivial exponent.eq_1 IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree Int.absNorm_under_eq_sInf
not_dvd_exponent_iff 📖	mathematical	—	exponent Codisjoint Ideal CommSemiring.toSemiring Int.instCommSemiring Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instOrderTop Ideal.comap NumberField.RingOfIntegers RingHom CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap Ring.toIntAlgebra CommRing.toRing RingHom.instRingHomClass conductor Int.instCommRing Ideal.span Set Set.instSingletonSet	—	RingHom.instRingHomClass codisjoint_comm IsCoatom.not_le_iff_codisjoint Ideal.isMaximal_def Int.ideal_span_isMaximal_of_prime Ideal.under_def IsScalarTower.right Ideal.dvd_iff_le IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Int.instNontrivial Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree Int.ideal_span_absNorm_eq_self span_singleton_dvd_span_singleton_iff_dvd exponent.eq_1

---

← Back to Index