Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `piQuotientEquiv`, `piQuotientLinearEquiv`, `algebraQuotientOfRamificationIdxNeZero`, `algebraQuotientPowRamificationIdx`, `powQuotSuccInclusion`, `quotientRangePowQuotSuccInclusionEquiv`, `quotientToQuotientRangePowQuotSucc`, `quotientToQuotientRangePowQuotSuccAux`	8
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`, `algebraMap_quotient_of_ramificationIdx_neZero`, `algebraMap_quotient_pow_ramificationIdx`, `card_primesOverFinset_le_finrank`, `finrank_prime_pow_ramificationIdx`, `finrank_quotient_map`, `inertiaDeg_le_finrank`, `powQuotSuccInclusion_apply_coe`, `powQuotSuccInclusion_injective`, `quotientToQuotientRangePowQuotSuccAux_mk`, `quotientToQuotientRangePowQuotSucc_injective`, `quotientToQuotientRangePowQuotSucc_mk`, `quotientToQuotientRangePowQuotSucc_surjective`, `ramificationIdx_le_finrank`, `ramificationIdx_mul_inertiaDeg_of_isLocalRing`, `rank_pow_quot`, `rank_pow_quot_aux`, `rank_prime_pow_ramificationIdx`, `sum_ramification_inertia`	30
Total	38

Ideal

Definitions

Name	Category	Theorems
`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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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` `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_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`
`powQuotSuccInclusion_apply_coe` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `ramificationIdx` `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` `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` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `instHasQuotient_1` `Ring.toSemiring` `instHasQuotient` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Quotient.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `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` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `Quotient.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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_le_finrank` 📖	mathematical	—	`ramificationIdx` `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_mul_inertiaDeg_of_isLocalRing` 📖	mathematical	—	`ramificationIdx` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `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`
`rank_pow_quot` 📖	mathematical	`ramificationIdx`	`Module.rank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `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.toNSMul` `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`	`Module.rank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx` `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` `Quotient.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Algebra.toModule` `Quotient.commSemiring` `Quotient.algebraQuotientPowRamificationIdx` `Cardinal` `AddMonoid.toNSMul` `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` `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` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Multiset.toFinset` `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_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` `Submodule.decidableEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `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` `Submodule.decidableEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.ramificationIdx` `Ideal.Quotient.semiring` `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` `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` `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` `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` `Submodule.Quotient.instSMul` `CommRing.toRing` `Ring.toAddCommGroup` `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` `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` `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` `Submodule.decidableEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Submodule.instPowNat` `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` `Submodule.decidableEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `UniqueFactorizationMonoid.factors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.uniqueFactorizationMonoid` `Submodule.instPowNat` `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`	`LinearIndependent` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `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`	`Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Top.top` `Submodule` `Submodule.instTop`	—	`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.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` `Semiring.toNonAssocSemiring` `commSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebraQuotientPowRamificationIdx` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `ring` `Ideal.instIsTwoSided_1`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1`

---

← Back to Index