Basic

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

Statistics

Metric	Count
Definitions `piQuotientEquiv`, `piQuotientLinearEquiv`, `algebraQuotientOfRamificationIdxNeZero`, `algebraQuotientPowRamificationIdx`, `inertiaDeg`, `powQuotSuccInclusion`, `quotientRangePowQuotSuccInclusionEquiv`, `quotientToQuotientRangePowQuotSucc`, `quotientToQuotientRangePowQuotSuccAux`, `ramificationIdx`	10
Theorems `fact_ramificationIdx_neZero`, `finiteDimensional_quotient_pow`, `finrank_pow_ramificationIdx`, `isPrime`, `isScalarTower`, `liesOver`, `ne_bot`, `piQuotientEquiv_map`, `piQuotientEquiv_mk`, `ramificationIdx_ne_zero`, `linearIndependent_of_nontrivial`, `span_eq_top`, `ramificationIdx_eq_factors_count`, `ramificationIdx_eq_multiplicity`, `ramificationIdx_eq_normalizedFactors_count`, `ramificationIdx_eq_one_iff`, `ramificationIdx_ne_zero`, `ramificationIdx_ne_zero_of_liesOver`, `algebraMap_quotient_of_ramificationIdx_neZero`, `algebraMap_quotient_pow_ramificationIdx`, `absNorm_eq_pow_inertiaDeg`, `absNorm_eq_pow_inertiaDeg'`, `absNorm_eq_pow_inertiaDeg_of_liesOver`, `card_primesOverFinset_le_finrank`, `finrank_prime_pow_ramificationIdx`, `finrank_quotient_map`, `inertiaDeg_algebraMap`, `inertiaDeg_algebra_tower`, `inertiaDeg_bot`, `inertiaDeg_comap_eq`, `inertiaDeg_le_finrank`, `inertiaDeg_map_eq`, `inertiaDeg_ne_zero`, `inertiaDeg_of_subsingleton`, `inertiaDeg_pos`, `le_comap_of_ramificationIdx_ne_zero`, `le_comap_pow_ramificationIdx`, `le_pow_of_le_ramificationIdx`, `le_pow_ramificationIdx`, `powQuotSuccInclusion_apply_coe`, `powQuotSuccInclusion_injective`, `quotientToQuotientRangePowQuotSuccAux_mk`, `quotientToQuotientRangePowQuotSucc_injective`, `quotientToQuotientRangePowQuotSucc_mk`, `quotientToQuotientRangePowQuotSucc_surjective`, `ramificationIdx_algebra_tower`, `ramificationIdx_bot`, `ramificationIdx_bot'`, `ramificationIdx_comap_eq`, `ramificationIdx_eq_find`, `ramificationIdx_eq_one_of_map_localization`, `ramificationIdx_eq_zero`, `ramificationIdx_le_finrank`, `ramificationIdx_lt`, `ramificationIdx_map_eq`, `ramificationIdx_map_self_eq_one`, `ramificationIdx_mul_inertiaDeg_of_isLocalRing`, `ramificationIdx_ne_one_iff`, `ramificationIdx_ne_zero`, `ramificationIdx_of_not_le`, `ramificationIdx_spec`, `ramificationIdx_tower`, `rank_pow_quot`, `rank_pow_quot_aux`, `rank_prime_pow_ramificationIdx`, `sum_ramification_inertia`	66
Total	76

Ideal

Definitions

Name	Category	Theorems
`inertiaDeg` 📖	CompOp	30 math math: `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `inertiaDeg_comap_eq`, `inertiaDeg_algebraMap`, `absNorm_eq_pow_inertiaDeg'`, `relNorm_eq_pow_of_isPrime_isGalois`, `absNorm_eq_pow_inertiaDeg_of_liesOver`, `IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg`, `sum_ramification_inertia`, `IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq`, `inertiaDeg_eq_of_isGalois`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one`, `IsCyclotomicExtension.Rat.inertiaDeg_eq`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'`, `inertiaDeg_eq_of_isGaloisGroup`, `inertiaDeg_pos`, `inertiaDeg_of_subsingleton`, `ramificationIdx_mul_inertiaDeg_of_isLocalRing`, `Factors.finrank_pow_ramificationIdx`, `inertiaDeg_bot`, `inertiaDeg_algebra_tower`, `inertiaDegIn_eq_inertiaDeg`, `absNorm_eq_pow_inertiaDeg`, `inertiaDeg_le_finrank`, `IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd`, `inertiaDeg_map_eq`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime`, `relNorm_eq_pow_of_isMaximal`
`powQuotSuccInclusion` 📖	CompOp	6 math math: `powQuotSuccInclusion_apply_coe`, `quotientToQuotientRangePowQuotSucc_mk`, `quotientToQuotientRangePowQuotSucc_surjective`, `quotientToQuotientRangePowQuotSucc_injective`, `powQuotSuccInclusion_injective`, `quotientToQuotientRangePowQuotSuccAux_mk`
`quotientRangePowQuotSuccInclusionEquiv` 📖	CompOp	—
`quotientToQuotientRangePowQuotSucc` 📖	CompOp	3 math math: `quotientToQuotientRangePowQuotSucc_mk`, `quotientToQuotientRangePowQuotSucc_surjective`, `quotientToQuotientRangePowQuotSucc_injective`
`quotientToQuotientRangePowQuotSuccAux` 📖	CompOp	1 math math: `quotientToQuotientRangePowQuotSuccAux_mk`
`ramificationIdx` 📖	CompOp	51 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`, `Algebra.isUnramifiedAt_iff_of_isDedekindDomain`, `Quotient.algebraMap_quotient_pow_ramificationIdx`, `ramificationIdxIn_eq_ramificationIdx`, `ramificationIdx_bot'`, `IsDedekindDomain.ramificationIdx_eq_one_iff`, `ramificationIdx_eq_zero`, `ramificationIdx_mul_inertiaDeg_of_isLocalRing`, `Factors.finrank_pow_ramificationIdx`, `ramificationIdx_eq_of_isGalois`, `map_algebraMap_eq_finset_prod_pow`, `ramificationIdx_of_not_le`, `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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_eq_pow_inertiaDeg` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring`	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toNatPow` `Nat.instMonoid` `inertiaDeg` `Int.instCommRing` `span` `Int.instSemiring` `Set` `Set.instSingletonSet` `Ring.toIntAlgebra` `CommRing.toRing`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `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` `absNorm_span_singleton` `Algebra.norm_self` `absNorm_eq_pow_inertiaDeg_of_liesOver` `span_singleton_prime` `Prime.ne_zero`
`absNorm_eq_pow_inertiaDeg'` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toNatPow` `Nat.instMonoid` `inertiaDeg` `Int.instCommRing` `span` `Int.instSemiring` `Set` `Set.instSingletonSet` `Ring.toIntAlgebra` `CommRing.toRing`	—	`absNorm_eq_pow_inertiaDeg` `Nat.prime_iff_prime_int`
`absNorm_eq_pow_inertiaDeg_of_liesOver` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Monoid.toNatPow` `Nat.instMonoid` `inertiaDeg`	—	`IsPrime.isMaximal` `IsDedekindDomainDvr.ring_dimensionLEOne` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsDomain.toNontrivial` `Submodule.cardQuot_apply` `inertiaDeg_algebraMap` `Module.natCard_eq_pow_finrank` `module_finite_of_liesOver`
`card_primesOverFinset_le_finrank` 📖	mathematical	—	`Finset.card` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `primesOverFinset` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`sum_ramification_inertia` `Finset.card_eq_sum_ones` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mem_primesOverFinset_iff` `IsDedekindDomain.toIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Right.one_le_mul` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver` `inertiaDeg_ne_zero`
`finrank_prime_pow_ramificationIdx` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `algebraMap` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Quotient.algebraQuotientOfRamificationIdxNeZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`IsScalarTower.right` `rank_prime_pow_ramificationIdx` `Module.finiteDimensional_iff_of_rank_eq_nsmul` `Nat.cast_injective` `Cardinal.instCharZero` `Module.finrank_eq_rank'` `Nat.cast_mul` `nsmul_eq_mul` `Module.finrank_of_infinite_dimensional` `MulZeroClass.mul_zero`
`finrank_quotient_map` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraQuotientMapQuotient` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semifield.toCommSemiring`	—	`Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Quotient.isDomain` `instIsTwoSided_1` `IsMaximal.isPrime'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `QuotientMapQuotient.isNoetherian` `isNoetherian_of_isNoetherianRing_of_finite` `IsDedekindDomainDvr.toIsNoetherian` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `Module.Projective.of_free` `Module.Free.of_divisionRing` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Quotient.mk_surjective` `IsScalarTower.right` `LinearMap.IsScalarTower.compatibleSMul'` `Quotient.isScalarTower` `Module.Basis.linearIndependent` `FinrankQuotientMap.linearIndependent_of_nontrivial` `Quotient.tower_quotient_map_quotient` `RingHom.instRingHomClass` `Quotient.algebraMap_eq` `mk_ker` `IsMaximal.ne_top` `IsFractionRing.injective` `Set.range_comp` `FinrankQuotientMap.span_eq_top` `Algebra.IsAlgebraic.of_finite` `IsDomain.toNontrivial` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toIsCancelMulZero` `instIsDomain` `top_le_iff` `Module.Basis.mem_span` `RingHomSurjective.ids` `Submodule.mem_map` `Submodule.map_span` `Submodule.restrictScalars_span` `Submodule.restrictScalars_mem` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.mem_sup_left` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `Submodule.mem_sup_right` `Submodule.Quotient.eq` `Submodule.mkQ_apply` `LinearMap.restrictScalars_apply` `neg_sub` `add_sub_cancel` `Eq.ge` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`inertiaDeg_algebraMap` 📖	mathematical	—	`inertiaDeg` `Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraOfLiesOver`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `inertiaDeg_of_subsingleton` `Module.finrank_zero_of_subsingleton` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsTwoSided_1` `inertiaDeg.eq_1` `over_def`
`inertiaDeg_algebra_tower` 📖	mathematical	—	`inertiaDeg`	—	`over_def` `LiesOver.over` `LiesOver.trans` `instIsTwoSided_1` `Eq.le` `Module.finrank_mul_finrank` `IsScalarTower.of_algebraMap_eq` `IsScalarTower.algebraMap_apply` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`inertiaDeg_bot` 📖	mathematical	—	`inertiaDeg` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Module.finrank` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`instIsTwoSided_1` `inertiaDeg.eq_1` `over_def` `eq_bot_of_liesOver_bot` `Algebra.finrank_eq_of_equiv_equiv` `instIsTwoSidedBot`
`inertiaDeg_comap_eq` 📖	mathematical	—	`inertiaDeg` `comap` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `EquivLike.toFunLike` `AlgEquiv.instEquivLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`	—	`RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `comap_coe` `comap_comap` `AlgHom.algHomClass` `AlgEquiv.toAlgHom_toRingHom` `AlgHom.comp_algebraMap` `comap_liesOver` `inertiaDeg_algebraMap` `LinearEquiv.finrank_eq` `instIsTwoSided_1` `inertiaDeg.eq_1`
`inertiaDeg_le_finrank` 📖	mathematical	—	`inertiaDeg` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`mem_primesOverFinset_iff` `IsDedekindDomain.toIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `sum_ramification_inertia` `Finset.add_sum_erase` `le_trans` `IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver`
`inertiaDeg_map_eq` 📖	mathematical	—	`inertiaDeg` `map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike`	—	`AlgEquivClass.toRingEquivClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_comap_of_equiv` `inertiaDeg_comap_eq`
`inertiaDeg_ne_zero` 📖	—	—	—	—	`inertiaDeg_pos`
`inertiaDeg_of_subsingleton` 📖	mathematical	—	`inertiaDeg`	—	`Quotient.subsingleton_iff` `IsMaximal.ne_top` `comap_top` `instIsTwoSided_1`
`inertiaDeg_pos` 📖	mathematical	—	`inertiaDeg`	—	`Quotient.nontrivial_of_liesOver_of_isPrime` `IsMaximal.isPrime'` `LT.lt.trans_eq` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `module_finite_of_liesOver` `Quotient.isDomain` `instIsTwoSided_1` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `inertiaDeg_algebraMap`
`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` `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` `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` `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` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `ramificationIdx`	—	`le_pow_of_le_ramificationIdx` `le_refl`
`powQuotSuccInclusion_apply_coe` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `ramificationIdx` `algebraMap` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map` `RingHom` `Quotient.ring` `RingHom.instFunLike` `DFunLike.coe` `LinearMap` `instHasQuotient_1` `RingHom.id` `IsScalarTower.right` `Algebra.id` `instIsTwoSided_1` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `LinearMap.instFunLike` `powQuotSuccInclusion`	—	`IsScalarTower.right` `instIsTwoSided_1`
`powQuotSuccInclusion_injective` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `algebraMap` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `DFunLike.coe` `LinearMap` `instHasQuotient_1` `RingHom.id` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `LinearMap.instFunLike` `powQuotSuccInclusion`	—	`IsScalarTower.right` `instIsTwoSided_1` `LinearMap.ker_eq_bot` `LinearMap.ker_eq_bot'` `powQuotSuccInclusion_apply_coe`
`quotientToQuotientRangePowQuotSuccAux_mk` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`quotientToQuotientRangePowQuotSuccAux` `CommRing.toRing` `Ring.toAddCommGroup` `HasQuotient.Quotient` `instHasQuotient_1` `Ring.toSemiring` `instHasQuotient` `ramificationIdx` `algebraMap` `Quotient.semiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Quotient.instRingQuotient` `Submodule.addCommGroup` `Submodule.Quotient.addCommGroup` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `LinearMap.range` `Submodule.addCommMonoid` `RingHom.id` `RingHomSurjective.ids` `powQuotSuccInclusion` `DFunLike.coe` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `mem_map_of_mem` `mul_mem_right`	—	`IsScalarTower.right` `Quotient.map'_mk''`
`quotientToQuotientRangePowQuotSucc_injective` 📖	mathematical	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`HasQuotient.Quotient` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Quotient.semiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Submodule` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `Submodule.hasQuotient` `Quotient.instRingQuotient` `Submodule.addCommGroup` `Submodule.Quotient.addCommGroup` `Ring.toAddCommGroup` `LinearMap.range` `RingHom.id` `RingHomSurjective.ids` `powQuotSuccInclusion` `DFunLike.coe` `LinearMap` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `AddCommGroup.toAddCommMonoid` `Quotient.algebraQuotientOfRamificationIdxNeZero` `Submodule.Quotient.module` `LinearMap.instFunLike` `quotientToQuotientRangePowQuotSucc`	—	`IsScalarTower.right` `Quotient.inductionOn'` `instIsTwoSided_1` `RingHomSurjective.ids` `pow_le_pow_right` `mem_map_of_mem` `mul_mem_right` `Submodule.coe_sub` `IsPrime.mem_pow_mul` `Submodule.sub_mem_iff_right` `sup_eq_left` `mem_quotient_iff_mem_sup` `mul_sub` `Quotient.eq` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `powQuotSuccInclusion_apply_coe`
`quotientToQuotientRangePowQuotSucc_mk` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`DFunLike.coe` `LinearMap` `HasQuotient.Quotient` `instHasQuotient_1` `Quotient.semiring` `RingHom.id` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `ramificationIdx` `algebraMap` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Submodule` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `Submodule.hasQuotient` `Quotient.instRingQuotient` `Submodule.addCommGroup` `Submodule.Quotient.addCommGroup` `Ring.toAddCommGroup` `LinearMap.range` `RingHomSurjective.ids` `powQuotSuccInclusion` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `AddCommGroup.toAddCommMonoid` `Quotient.algebraQuotientOfRamificationIdxNeZero` `Submodule.Quotient.module` `LinearMap.instFunLike` `quotientToQuotientRangePowQuotSucc` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `mem_map_of_mem` `mul_mem_right`	—	`IsScalarTower.right`
`quotientToQuotientRangePowQuotSucc_surjective` 📖	mathematical	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`HasQuotient.Quotient` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Quotient.semiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Submodule` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `Submodule.hasQuotient` `Quotient.instRingQuotient` `Submodule.addCommGroup` `Submodule.Quotient.addCommGroup` `Ring.toAddCommGroup` `LinearMap.range` `RingHom.id` `RingHomSurjective.ids` `powQuotSuccInclusion` `DFunLike.coe` `LinearMap` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `AddCommGroup.toAddCommMonoid` `Quotient.algebraQuotientOfRamificationIdxNeZero` `Submodule.Quotient.module` `LinearMap.instFunLike` `quotientToQuotientRangePowQuotSucc`	—	`IsScalarTower.right` `instIsTwoSided_1` `RingHomSurjective.ids` `pow_le_pow_right` `LT.lt.le` `uniqueFactorizationMonoid` `sup_eq_prod_inf_factors` `zero_mem` `span_singleton_eq_bot` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `UniqueFactorizationMonoid.normalizedFactors_pow` `UniqueFactorizationMonoid.normalizedFactors_irreducible` `Prime.irreducible` `isCancelMulZero` `prime_iff_isPrime` `normalize_eq` `Multiset.nsmul_singleton` `Multiset.inter_replicate` `Multiset.prod_replicate` `count_normalizedFactors_eq` `submodule_span_eq` `Submodule.span_singleton_le_iff_mem` `min_eq_left` `sup_eq_left` `mem_quotient_iff_mem_sup` `Submodule.mem_sup` `mem_span_singleton` `mem_map_of_mem` `mul_mem_right` `Submodule.coe_sub` `Submodule.neg_mem` `powQuotSuccInclusion_apply_coe` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_add_cancel_left` `map_neg`
`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`	—	`IsScalarTower.algebraMap_eq` `ramificationIdx_tower`
`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`	`ramificationIdx` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`ramificationIdx_of_not_le` `Iff.not` `le_bot_iff` `map_eq_bot_iff_of_injective` `RingHom.instRingHomClass`
`ramificationIdx_comap_eq` 📖	mathematical	—	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `comap` `AlgEquiv` `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` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`ramificationIdx`	—	`IsScalarTower.right` `Mathlib.Tactic.Push.not_forall_eq`
`ramificationIdx_le_finrank` 📖	mathematical	—	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`ramificationIdx_bot` `Nat.instCanonicallyOrderedAdd` `mem_primesOverFinset_iff` `IsDedekindDomain.toIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `sum_ramification_inertia` `Finset.add_sum_erase` `le_trans` `inertiaDeg_ne_zero`
`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` `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` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `map` `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`	—	`ramificationIdx_spec` `IsScalarTower.right` `pow_one` `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_mul_inertiaDeg_of_isLocalRing` 📖	mathematical	—	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `IsLocalRing.maximalIdeal` `inertiaDeg` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`FaithfulSMul.of_field_isFractionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `sum_ramification_inertia` `Finset.sum_congr` `IsLocalRing.primesOverFinset_eq` `IsDedekindDomain.toIsDomain` `Finset.sum_singleton`
`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`	`Monoid.toNatPow` `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` `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`	`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` `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`	`ramificationIdx` `RingHom.comp`	—	`ne_bot_of_map_ne_bot` `RingHom.instRingHomClass` `map_map` `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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sup_le` `le_of_dvd` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `Multiset.count_ne_zero`
`rank_pow_quot` 📖	mathematical	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Module.rank` `HasQuotient.Quotient` `Ideal` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `Cardinal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Cardinal.commSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Quotient.algebraQuotientOfRamificationIdxNeZero`	—	`IsScalarTower.right` `instIsTwoSided_1` `rank_pow_quot_aux` `succ_nsmul'` `zero_nsmul` `map_quotient_self` `rank_bot` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`rank_pow_quot_aux` 📖	mathematical	`ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Module.rank` `HasQuotient.Quotient` `Ideal` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map` `RingHom` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Algebra.toModule` `Cardinal` `Cardinal.instAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Quotient.algebraQuotientOfRamificationIdxNeZero`	—	`IsScalarTower.right` `instIsTwoSided_1` `RingHomSurjective.ids` `rank_range_of_injective` `powQuotSuccInclusion_injective` `LinearEquiv.rank_eq` `RingHomInvPair.ids` `Submodule.rank_quotient_add_rank` `IsDomain.hasRankNullity` `Quotient.isDomain` `IsMaximal.isPrime'`
`rank_prime_pow_ramificationIdx` 📖	mathematical	—	`Module.rank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `algebraMap` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Cardinal` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Cardinal.commSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Quotient.algebraQuotientOfRamificationIdxNeZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`IsScalarTower.right` `instIsTwoSided_1` `rank_pow_quot` `rank_top` `map_top` `RingHom.instRingHomClass` `one_eq_top` `pow_zero`
`sum_ramification_inertia` 📖	mathematical	—	`Finset.sum` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddCommMonoid` `primesOverFinset` `ramificationIdx` `algebraMap` `inertiaDeg` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`uniqueFactorizationMonoid` `IsScalarTower.right` `Finset.sum_attach` `Finset.sum_congr` `Factors.finrank_pow_ramificationIdx` `Module.finrank_pi_fintype` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Quotient.isDomain` `instIsTwoSided_1` `IsMaximal.isPrime'` `Factors.finiteDimensional_quotient_pow` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LinearEquiv.finrank_eq` `RingHomInvPair.ids` `RingHom.instRingHomClass` `map_eq_bot_iff_le_ker` `RingHom.injective_iff_ker_eq_bot` `algebraMap_injective_of_field_isFractionRing` `le_bot_iff` `finrank_quotient_map` `IsDedekindDomain.toIsDomain`

Ideal.Factors

Definitions

Name	Category	Theorems
`piQuotientEquiv` 📖	CompOp	2 math math: `piQuotientEquiv_mk`, `piQuotientEquiv_map`
`piQuotientLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fact_ramificationIdx_neZero` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `Ideal.ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`Ideal.uniqueFactorizationMonoid` `ramificationIdx_ne_zero`
`finiteDimensional_quotient_pow` 📖	mathematical	—	`FiniteDimensional` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.ramificationIdx` `Field.toDivisionRing` `Ideal.Quotient.field` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `Algebra.toModule` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `Ideal.Quotient.algebraQuotientPowRamificationIdx`	—	`Ideal.uniqueFactorizationMonoid` `FiniteDimensional.of_finrank_pos` `IsScalarTower.right` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `finrank_pow_ramificationIdx` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `ramificationIdx_ne_zero` `LT.lt.ne'` `Ideal.inertiaDeg_pos` `liesOver`
`finrank_pow_ramificationIdx` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.ramificationIdx` `Ideal.Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Algebra.toModule` `Ideal.Quotient.commSemiring` `Ideal.Quotient.algebraQuotientPowRamificationIdx` `Ideal.inertiaDeg`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.right` `fact_ramificationIdx_neZero` `Ideal.finrank_prime_pow_ramificationIdx` `ne_bot` `isPrime` `liesOver` `Ideal.inertiaDeg_algebraMap`
`isPrime` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`Ideal.uniqueFactorizationMonoid` `Ideal.isPrime_of_prime` `UniqueFactorizationMonoid.prime_of_factor` `Multiset.mem_toFinset`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Submodule.Quotient.instSMul` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero` `fact_ramificationIdx_neZero` `Submodule.Quotient.instSMul'` `IsScalarTower.right`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.of_algebraMap_eq'` `fact_ramificationIdx_neZero`
`liesOver` 📖	mathematical	—	`Ideal.LiesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`Ideal.uniqueFactorizationMonoid` `RingHom.instRingHomClass` `Ideal.comap_eq_of_scalar_tower_quotient` `fact_ramificationIdx_neZero` `isScalarTower` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial` `Ideal.instIsTwoSided_1` `Ideal.Quotient.isDomain` `isPrime`
`ne_bot` 📖	—	—	—	—	`Ideal.uniqueFactorizationMonoid` `Prime.ne_zero` `UniqueFactorizationMonoid.prime_of_factor` `Multiset.mem_toFinset`
`piQuotientEquiv_map` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Pi.instMul` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.ramificationIdx` `Distrib.toAdd` `Pi.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `piQuotientEquiv` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.right`
`piQuotientEquiv_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Pi.instMul` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.ramificationIdx` `Distrib.toAdd` `Pi.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `piQuotientEquiv` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.right` `Ideal.instIsTwoSided_1`
`ramificationIdx_ne_zero` 📖	—	—	—	—	`Ideal.uniqueFactorizationMonoid` `Ideal.IsDedekindDomain.ramificationIdx_ne_zero` `UniqueFactorizationMonoid.ne_zero_of_mem_factors` `Multiset.mem_toFinset` `isPrime` `Ideal.le_of_dvd` `UniqueFactorizationMonoid.dvd_of_mem_factors`

Ideal.FinrankQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_of_nontrivial` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LinearIndependent`	`DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`RingHom.instRingHomClass` `Mathlib.Tactic.Contrapose.contrapose₁` `Ideal.exist_integer_multiples_notMem` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_zero` `Finset.smul_sum` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `IsScalarTower.algebraMap_smul` `smul_assoc` `IsScalarTower.left` `smul_eq_mul` `LinearMap.map_eq_zero_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`span_eq_top` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Submodule.span` `Submodule.restrictScalars` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Algebra.toSMul` `IsScalarTower.right` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap` `Top.top` `Submodule.instTop`	`DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semifield.toCommSemiring` `Set.image` `DFunLike.coe`	—	`IsScalarTower.right` `IsScalarTower.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Module.Finite.exists_fin` `Module.Finite.quotient` `Submodule.Quotient.isScalarTower` `IsScalarTower.left` `RingHomSurjective.ids` `Submodule.map_smul''` `Submodule.map_top` `Submodule.range_mkQ` `Ideal.smul_top_eq_map` `Submodule.map_mkQ_eq_top` `Submodule.mem_ideal_smul_span_iff_exists_sum` `Ideal.instIsTwoSided_1` `Submodule.mem_top` `Finsupp.sum_fintype` `zero_smul` `Finset.sum_congr` `sub_smul` `ite_smul` `one_smul` `Finset.sum_sub_distrib` `Finset.sum_ite_eq` `sub_self` `Matrix.adjugate_mul` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_smul` `Finset.smul_sum` `smul_smul` `Finset.sum_comm` `Finset.sum_eq_zero` `smul_zero` `Submodule.mem_span_singleton` `Submodule.restrictScalars_mem` `smul_eq_mul` `mul_comm` `Algebra.smul_def` `Submodule.Quotient.mk_eq_zero` `Submodule.Quotient.mk_smul` `SMulCommClass.smul_comm` `Submodule.Quotient.smulCommClass` `smulCommClass_self` `Finset.sum_const_zero` `top_le_iff` `Submodule.restrictScalars_eq_top_iff` `Ideal.span_singleton_eq_top` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ne_zero_of_map` `Ideal.Quotient.nontrivial_iff` `RingHom.map_det` `Matrix.ext` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.mapMatrix_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `Ideal.Quotient.eq_zero_iff_mem` `zero_sub` `Matrix.neg_apply` `Matrix.det_neg` `Fintype.card_fin` `Matrix.det_one` `IsUnit.ne_zero` `IsUnit.pow` `IsUnit.neg` `isUnit_one` `IsFractionRing.ideal_span_singleton_map_subset` `IsScalarTower.algebraMap_apply`

Ideal.IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ramificationIdx_eq_factors_count` 📖	mathematical	—	`Ideal.ramificationIdx` `Multiset.count` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`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`	—	`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` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`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` `Localization.AtPrime` `OreLocalization.instSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `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`	—	—	`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`

Ideal.Quotient

Definitions

Name	Category	Theorems
`algebraQuotientOfRamificationIdxNeZero` 📖	CompOp	9 math math: `Ideal.rank_prime_pow_ramificationIdx`, `algebraMap_quotient_of_ramificationIdx_neZero`, `Ideal.Factors.isScalarTower`, `Ideal.quotientToQuotientRangePowQuotSucc_mk`, `Ideal.finrank_prime_pow_ramificationIdx`, `Ideal.quotientToQuotientRangePowQuotSucc_surjective`, `Ideal.quotientToQuotientRangePowQuotSucc_injective`, `Ideal.rank_pow_quot_aux`, `Ideal.rank_pow_quot`
`algebraQuotientPowRamificationIdx` 📖	CompOp	13 math math: `Ideal.rank_prime_pow_ramificationIdx`, `Ideal.powQuotSuccInclusion_apply_coe`, `Ideal.quotientToQuotientRangePowQuotSucc_mk`, `Ideal.finrank_prime_pow_ramificationIdx`, `Ideal.quotientToQuotientRangePowQuotSucc_surjective`, `algebraMap_quotient_pow_ramificationIdx`, `Ideal.quotientToQuotientRangePowQuotSucc_injective`, `Ideal.Factors.finrank_pow_ramificationIdx`, `Ideal.rank_pow_quot_aux`, `Ideal.rank_pow_quot`, `Ideal.powQuotSuccInclusion_injective`, `Ideal.Factors.finiteDimensional_quotient_pow`, `Ideal.quotientToQuotientRangePowQuotSuccAux_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_quotient_of_ramificationIdx_neZero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Semiring.toNonAssocSemiring` `commSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebraQuotientOfRamificationIdxNeZero` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1`
`algebraMap_quotient_pow_ramificationIdx` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.ramificationIdx` `algebraMap` `Semiring.toNonAssocSemiring` `commSemiring` `semiring` `RingHom.instFunLike` `algebraQuotientPowRamificationIdx` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `ring` `Ideal.instIsTwoSided_1`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1`

---

← Back to Index