Ramification

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

Statistics

Metric	Count
Definitions ramificationIdx	1
Theorems emultiplicity_map_eq_ramificationIdx_mul, emultiplicity_map_eq_zero_of_ne, ramificationIdx_eq_factors_count, ramificationIdx_eq_multiplicity, ramificationIdx_eq_normalizedFactors_count, ramificationIdx_eq_one_iff, ramificationIdx_ne_zero, ramificationIdx_ne_zero_of_liesOver, le_comap_of_ramificationIdx_ne_zero, le_comap_pow_ramificationIdx, le_pow_of_le_ramificationIdx, le_pow_ramificationIdx, ramificationIdx_algebra_tower, ramificationIdx_algebra_tower', ramificationIdx_bot, ramificationIdx_bot', ramificationIdx_comap_eq, ramificationIdx_eq_find, ramificationIdx_eq_one_of_map_localization, ramificationIdx_eq_zero, ramificationIdx_lt, ramificationIdx_map_eq, ramificationIdx_map_self_eq_one, ramificationIdx_ne_one_iff, ramificationIdx_ne_zero, ramificationIdx_of_not_le, ramificationIdx_spec, ramificationIdx_tower	28
Total	29

Ideal

Definitions

Name	Category	Theorems
ramificationIdx 📖	CompOp	57 math math: NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', ramificationIdx_comap_eq, rank_prime_pow_ramificationIdx, ramificationIdx_le_finrank, ramificationIdx_eq_one_of_isUnramifiedAt, Factors.fact_ramificationIdx_neZero, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, powQuotSuccInclusion_apply_coe, IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, sum_ramification_inertia, ramificationIdx_algebra_tower, ramificationIdx_bot, ramificationIdx_eq_find, quotientToQuotientRangePowQuotSucc_mk, finrank_prime_pow_ramificationIdx, le_pow_ramificationIdx, ramificationIdx_map_eq, ramificationIdx_spec, ramificationIdx_eq_one_of_map_localization, IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq, ramificationIdx_tower, quotientToQuotientRangePowQuotSucc_surjective, Algebra.isUnramifiedAt_iff_of_isDedekindDomain, Quotient.algebraMap_quotient_pow_ramificationIdx, ramificationIdxIn_eq_ramificationIdx, ramificationIdx_bot', quotientToQuotientRangePowQuotSucc_injective, IsDedekindDomain.ramificationIdx_eq_one_iff, ramificationIdx_eq_zero, ramificationIdx_mul_inertiaDeg_of_isLocalRing, Factors.finrank_pow_ramificationIdx, rank_pow_quot_aux, ramificationIdx_eq_of_isGalois, map_algebraMap_eq_finset_prod_pow, ramificationIdx_of_not_le, rank_pow_quot, powQuotSuccInclusion_injective, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, IsDedekindDomain.ramificationIdx_eq_factors_count, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, Factors.finiteDimensional_quotient_pow, IsCyclotomicExtension.Rat.ramificationIdx_eq, ramificationIdx_lt, IsDedekindDomain.ramificationIdx_eq_multiplicity, quotientToQuotientRangePowQuotSuccAux_mk, Factors.piQuotientEquiv_mk, ramificationIdx_eq_of_isGaloisGroup, IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, ramificationIdx_map_self_eq_one, le_comap_pow_ramificationIdx, Factors.piQuotientEquiv_map, ramificationIdx_algebra_tower', IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_comap_of_ramificationIdx_ne_zero 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	RingHom.instRingHomClass map_le_iff_le_comap LE.le.trans IsScalarTower.right le_pow_ramificationIdx pow_le_self
le_comap_pow_ramificationIdx 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass Submodule.instPowNat IsScalarTower.right Algebra.id ramificationIdx	—	IsScalarTower.right RingHom.instRingHomClass map_le_iff_le_comap le_pow_ramificationIdx
le_pow_of_le_ramificationIdx 📖	mathematical	ramificationIdx	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id	—	Mathlib.Tactic.Contrapose.contrapose₁ IsScalarTower.right ramificationIdx_lt
le_pow_ramificationIdx 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id ramificationIdx	—	le_pow_of_le_ramificationIdx le_refl
ramificationIdx_algebra_tower 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap	ramificationIdx	—	ne_bot_of_map_ne_bot RingHom.instRingHomClass map_map IsScalarTower.algebraMap_eq ne_bot_of_le_ne_bot uniqueFactorizationMonoid IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count IsScalarTower.right eq_prime_pow_mul_coprime Ring.DimensionLEOne.maximalOfPrime IsDedekindDomainDvr.ring_dimensionLEOne IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr map_sup map_top IsPrime.ne_top eq_top_iff_one IsScalarTower.left map_mul map_pow UniqueFactorizationMonoid.normalizedFactors_mul pow_ne_zero isReduced_of_noZeroDivisors instNoZeroDivisors IsDomain.to_noZeroDivisors Eq.trans_le sup_of_le_left Multiset.count_add UniqueFactorizationMonoid.normalizedFactors_pow Multiset.count_nsmul add_eq_left instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid sup_le le_of_dvd UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors Multiset.count_ne_zero
ramificationIdx_algebra_tower' 📖	mathematical	—	ramificationIdx	—	eq_or_ne ramificationIdx_bot MulZeroClass.zero_mul IsPrime.under over_def Module.IsTorsionFree.of_smul_eq_zero IsDomain.toNontrivial FaithfulSMul.algebraMap_eq_zero_iff Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDedekindDomain.toIsDomain smul_eq_zero algebra_compatible_smul ne_bot_of_liesOver_of_ne_bot ramificationIdx_algebra_tower map_ne_bot_of_ne_bot map_le_iff_le_comap le_of_eq
ramificationIdx_bot 📖	mathematical	—	ramificationIdx Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	LT.lt.not_ge map_bot RingHom.instRingHomClass
ramificationIdx_bot' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	ramificationIdx Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	ramificationIdx_of_not_le Iff.not le_bot_iff map_eq_bot_iff_of_injective RingHom.instRingHomClass
ramificationIdx_comap_eq 📖	mathematical	—	ramificationIdx comap AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike AlgHomClass.toRingHomClass EquivLike.toFunLike AlgEquiv.instEquivLike AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Set.ext RingHom.instRingHomClass comap_coe RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass AlgEquivClass.toRingEquivClass AlgEquiv.toRingEquiv_toRingHom RingEquiv.symm_symm map_comap_of_equiv IsScalarTower.right map_pow comap_comap AlgHom.algHomClass AlgEquiv.toAlgHom_toRingHom AlgHom.comp_algebraMap
ramificationIdx_eq_find 📖	mathematical	—	ramificationIdx Nat.find	—	IsScalarTower.right Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable Nat.sSup_def
ramificationIdx_eq_one_of_map_localization 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instPartialOrder primeCompl nonZeroDivisors Semiring.toMonoidWithZero Localization.AtPrime OreLocalization.instSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAlgebra IsLocalRing.maximalIdeal OreLocalization.instCommSemiring Localization.AtPrime.isLocalRing	ramificationIdx	—	Localization.AtPrime.isLocalRing not_ne_iff ramificationIdx_ne_one_iff map_mono Submodule.eq_bot_of_le_smul_of_le_jacobson_bot IsNoetherian.noetherian IsLocalization.instIsNoetherianRingLocalization pow_two IsScalarTower.right IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower map_map Localization.AtPrime.map_eq_maximalIdeal map_pow RingHom.instRingHomClass IsLocalRing.maximalIdeal_le_jacobson map_eq_bot_iff_of_injective IsLocalization.injective Localization.isLocalization
ramificationIdx_eq_zero 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id	ramificationIdx	—	IsScalarTower.right Mathlib.Tactic.Push.not_forall_eq
ramificationIdx_lt 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id	ramificationIdx	—	IsScalarTower.right pow_zero one_eq_top le_of_not_gt LE.le.trans pow_le_pow_right ramificationIdx_eq_find Nat.find_min'
ramificationIdx_map_eq 📖	mathematical	—	ramificationIdx map CommSemiring.toSemiring CommRing.toCommSemiring EquivLike.toFunLike	—	AlgEquivClass.toRingEquivClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_comap_of_equiv ramificationIdx_comap_eq
ramificationIdx_map_self_eq_one 📖	mathematical	—	ramificationIdx map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	ramificationIdx_spec IsScalarTower.right pow_one instReflLe le_antisymm pow_le_self two_ne_zero IsMulTorsionFree.pow_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero isCancelMulZero UniqueFactorizationMonoid.instIsMulTorsionFree uniqueFactorizationMonoid Subsingleton.to_isMulTorsionFree Unique.instSubsingleton one_eq_top Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
ramificationIdx_ne_one_iff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	—	IsScalarTower.right ramificationIdx_eq_zero IsScalarTower.left LE.le.trans pow_le_pow_right LT.lt.le Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq ramificationIdx_eq_find Nat.find_spec pow_one Nat.find_min
ramificationIdx_ne_zero 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id	—	—	IsScalarTower.right ramificationIdx_spec
ramificationIdx_of_not_le 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap	ramificationIdx	—	ramificationIdx_spec IsScalarTower.right pow_zero one_eq_top zero_add pow_one
ramificationIdx_spec 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap Submodule.instPowNat IsScalarTower.right Algebra.id	ramificationIdx	—	IsScalarTower.right le_of_not_gt LE.le.trans pow_le_pow_right ramificationIdx_eq_find le_antisymm Nat.find_min' LT.lt.not_ge Nat.find_spec
ramificationIdx_tower 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap	ramificationIdx	—	ramificationIdx_algebra_tower

Ideal.IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
emultiplicity_map_eq_ramificationIdx_mul 📖	mathematical	Irreducible Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	emultiplicity Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap ENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring instCommSemiringENat ENat.instNatCast Ideal.ramificationIdx	—	UniqueFactorizationMonoid.induction_on_prime Ideal.uniqueFactorizationMonoid Ideal.map_top RingHom.instRingHomClass UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors top_ne_bot Ideal.instNontrivial IsDomain.toNontrivial IsDedekindDomain.toIsDomain Multiset.count.congr_simp UniqueFactorizationMonoid.normalizedFactors.congr_simp UniqueFactorizationMonoid.normalizedFactors_one normalize_eq Multiset.count_eq_zero_of_notMem CharP.cast_eq_zero CharP.ofCharZero MulZeroClass.mul_zero IsScalarTower.right IsScalarTower.left Ideal.map_mul emultiplicity_mul Ideal.isCancelMulZero Irreducible.prime UniqueFactorizationMonoid.instDecompositionMonoid mul_add Distrib.leftDistribClass
emultiplicity_map_eq_zero_of_ne 📖	mathematical	Irreducible Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Prime CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring	emultiplicity Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instCommSemiringENat	—	emultiplicity_eq_zero Ideal.IsMaximal.eq_of_le Ideal.IsPrime.isMaximal IsDedekindDomainDvr.ring_dimensionLEOne IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr Ideal.isPrime_of_prime Prime.ne_zero Ideal.IsPrime.ne_top Irreducible.prime UniqueFactorizationMonoid.instDecompositionMonoid Ideal.uniqueFactorizationMonoid Ideal.over_def RingHom.instRingHomClass Ideal.under_def Ideal.map_le_iff_le_comap IsScalarTower.right Ideal.dvd_iff_le
ramificationIdx_eq_factors_count 📖	mathematical	—	Ideal.ramificationIdx Multiset.count Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.decidableEq NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule UniqueFactorizationMonoid.factors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.uniqueFactorizationMonoid Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	Ideal.uniqueFactorizationMonoid ramificationIdx_eq_normalizedFactors_count Unique.instSubsingleton UniqueFactorizationMonoid.factors_eq_normalizedFactors
ramificationIdx_eq_multiplicity 📖	mathematical	—	Ideal.ramificationIdx multiplicity Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	Ideal.zero_eq_bot multiplicity_zero_eq_zero_of_ne_zero Ideal.ramificationIdx_of_not_le le_bot_iff multiplicity_eq_of_emultiplicity_eq_some Ideal.uniqueFactorizationMonoid ramificationIdx_eq_normalizedFactors_count Unique.instSubsingleton normalize_eq UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors irreducible_iff_prime Ideal.isCancelMulZero UniqueFactorizationMonoid.instDecompositionMonoid Ideal.prime_of_isPrime
ramificationIdx_eq_normalizedFactors_count 📖	mathematical	—	Ideal.ramificationIdx Multiset.count Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.decidableEq NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule UniqueFactorizationMonoid.normalizedFactors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.normalizationMonoid Ideal.uniqueFactorizationMonoid Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	Prime.irreducible Ideal.isCancelMulZero Ideal.prime_of_isPrime Ideal.ramificationIdx_spec Ideal.uniqueFactorizationMonoid Ideal.le_of_dvd IsScalarTower.right UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors pow_ne_zero isReduced_of_noZeroDivisors Ideal.instNoZeroDivisors IsDomain.to_noZeroDivisors IsDedekindDomain.toIsDomain UniqueFactorizationMonoid.normalizedFactors_pow UniqueFactorizationMonoid.normalizedFactors_irreducible normalize_eq Multiset.nsmul_singleton Multiset.le_count_iff_replicate_le le_refl Ideal.dvd_iff_le LT.lt.not_ge
ramificationIdx_eq_one_iff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike algebraMap	Ideal.ramificationIdx Ideal.map Localization.AtPrime CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra IsLocalRing.maximalIdeal OreLocalization.instCommSemiring Localization.AtPrime.isLocalRing	—	Localization.AtPrime.isLocalRing not_ne_iff Ideal.ramificationIdx_ne_one_iff pow_two IsScalarTower.right Ideal.dvd_iff_le Eq.trans_le Ideal.mul_mono_right IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower Ideal.map_map IsScalarTower.left Ideal.map_mul RingHom.instRingHomClass Localization.AtPrime.map_eq_maximalIdeal IsLocalization.map_algebraMap_ne_top_iff_disjoint Localization.isLocalization instIsConcreteLE Ideal.mul_top Ideal.instIsTwoSided_1 Ideal.ramificationIdx_eq_one_of_map_localization IsDedekindDomainDvr.toIsNoetherian IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors
ramificationIdx_ne_zero 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike algebraMap	—	—	le_bot_iff Prime.irreducible Ideal.isCancelMulZero Ideal.prime_of_isPrime Ideal.uniqueFactorizationMonoid ramificationIdx_eq_normalizedFactors_count UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd IsScalarTower.right Ideal.dvd_iff_le Multiset.count_ne_zero associated_iff_eq Unique.instSubsingleton
ramificationIdx_ne_zero_of_liesOver 📖	—	—	—	—	ramificationIdx_ne_zero Ideal.map_ne_bot_of_ne_bot IsDomain.toNontrivial IsDedekindDomain.toIsDomain Ideal.map_le_iff_le_comap le_of_eq Ideal.liesOver_iff

---

← Back to Index