Factorization

📁 Source: Mathlib/RingTheory/DedekindDomain/Factorization.lean

Statistics

Metric	Count
Definitions `count`, `divMod`, `quotientEquiv`, `maxPowDividing`	4
Theorems `finite_factors`, `finprod_ne_zero`, `count_coe`, `count_coe_nonneg`, `count_finprod`, `count_finprod_coprime`, `count_finsuppProd`, `count_inv`, `count_maximal`, `count_maximal_coprime`, `count_mono`, `count_mul`, `count_mul'`, `count_ne_zero`, `count_neg_zpow`, `count_one`, `count_pow`, `count_pow_self`, `count_prod`, `count_self`, `count_well_defined`, `count_zero`, `count_zpow`, `count_zpow_self`, `divMod_spec`, `divMod_zero_left`, `divMod_zero_of_not_le`, `divMod_zero_right`, `finite_factors`, `finite_factors'`, `finprod_heightOneSpectrum_factorization`, `finprod_heightOneSpectrum_factorization'`, `finprod_heightOneSpectrum_factorization_principal`, `finprod_heightOneSpectrum_factorization_principal_fraction`, `zero_divMod`, `finite_factors`, `finite_mulSupport`, `finite_mulSupport_coe`, `finite_mulSupport_inv`, `finprod_count`, `finprod_heightOneSpectrum_factorization`, `finprod_heightOneSpectrum_factorization_coe`, `finprod_not_dvd`, `map_algebraMap_eq_finset_prod_pow`, `maxPowDividing_eq_pow_multiset_count`, `exists_add_spanSingleton_mul_eq`, `exists_eq_span_pair`, `exists_sup_span_eq`	48
Total	52

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_factors` 📖	mathematical	—	`Filter.Eventually` `IsDedekindDomain.HeightOneSpectrum` `count` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `instCommMonoidWithZero` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `factors` `Ideal.uniqueFactorizationMonoid` `Filter.cofinite`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.right` `Set.ext` `count_ne_zero_iff_dvd` `IsDedekindDomain.HeightOneSpectrum.irreducible` `Filter.eventually_cofinite` `Ideal.finite_factors`
`finprod_ne_zero` 📖	—	—	—	—	`mk_ne_zero` `finprod_def` `Finset.prod_ne_zero_iff` `Ideal.instNontrivial` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Ideal.uniqueFactorizationMonoid` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `one_ne_zero` `NeZero.one`

FractionalIdeal

Definitions

Name	Category	Theorems
`count` 📖	CompOp	24 math math: `count_well_defined`, `count_finsuppProd`, `count_coe_nonneg`, `count_mono`, `count_finprod_coprime`, `count_prod`, `count_finprod`, `count_ne_zero`, `count_maximal_coprime`, `count_mul`, `count_pow`, `count_zpow_self`, `count_neg_zpow`, `count_zero`, `count_one`, `count_zpow`, `count_pow_self`, `count_inv`, `count_mul'`, `count_self`, `count_maximal`, `finite_factors`, `count_coe`, `finprod_heightOneSpectrum_factorization'`
`divMod` 📖	CompOp	5 math math: `divMod_zero_left`, `divMod_zero_of_not_le`, `divMod_zero_right`, `divMod_spec`, `zero_divMod`
`quotientEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_coe` 📖	mathematical	—	`count` `coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.factors` `Ideal.uniqueFactorizationMonoid`	—	`Ideal.uniqueFactorizationMonoid` `count_well_defined` `spanSingleton.congr_simp` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `inv_one` `spanSingleton_one` `one_mul` `Ideal.span_singleton_one` `sub_eq_self` `Nat.cast_eq_zero` `Int.instCharZero` `Ideal.one_eq_top` `Associates.mk_one` `Associates.factors_one` `Ideal.instNontrivial` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Associates.count_zero` `IsDedekindDomain.HeightOneSpectrum.associates_irreducible`
`count_coe_nonneg` 📖	mathematical	—	`count` `coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`count.congr_simp` `count_zero` `Ideal.uniqueFactorizationMonoid` `count_coe` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`
`count_finprod` 📖	mathematical	—	`count` `finprod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`Set.Finite.mem_toFinset` `finprod_eq_finset_prod_of_mulSupport_subset` `Set.Finite.coe_toFinset` `zpow_zero` `Function.mem_mulSupport` `Finsupp.prod.eq_1` `count_finsuppProd`
`count_finprod_coprime` 📖	mathematical	—	`count` `finprod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`finprod_mem_induction` `count_one` `count_mul'` `add_zero` `count_zpow` `count_maximal_coprime` `MulZeroClass.mul_zero`
`count_finsuppProd` 📖	mathematical	—	`count` `Finsupp.prod` `IsDedekindDomain.HeightOneSpectrum` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike`	—	`Finsupp.prod.eq_1` `count_prod` `zpow_ne_zero` `coeIdeal_ne_zero` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `Finset.sum_congr` `count_zpow` `count_maximal` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `Finsupp.mem_support_iff`
`count_inv` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain`	—	`IsDedekindDomain.toIsDomain` `zpow_neg_one` `count_neg_zpow` `zpow_one`
`count_maximal` 📖	mathematical	—	`count` `coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `IsDedekindDomain.HeightOneSpectrum`	—	`count_self` `count_maximal_coprime`
`count_maximal_coprime` 📖	mathematical	—	`count` `coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`RingHom.map_one` `inv_one` `spanSingleton_one` `one_mul` `coeIdeal_ne_zero` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `IsDedekindDomain.HeightOneSpectrum.associates_irreducible` `Ideal.uniqueFactorizationMonoid` `count_well_defined` `Ideal.span_singleton_one` `Ideal.one_eq_top` `Associates.mk_one` `Associates.factors_one` `Ideal.instNontrivial` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Associates.count_zero` `sub_zero` `pow_one` `Associates.factors_prime_pow` `Associates.count_some` `Multiset.replicate_one` `Multiset.count_eq_zero` `Multiset.mem_singleton` `Associates.mk_eq_mk_iff_associated` `associated_iff_eq` `Unique.instSubsingleton` `IsDedekindDomain.HeightOneSpectrum.ext_iff`
`count_mono` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`count`	—	`le_zero_iff` `LE.le.trans` `Eq.le` `IsDedekindDomain.toIsDomain` `mul_le_mul_right` `instMulLeftMono` `le_one_iff_exists_coeIdeal` `inv_mul_cancel₀` `mul_inv_cancel_left₀` `count_mul` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `inv_ne_zero` `le_add_iff_nonneg_right` `Int.instAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `count_coe_nonneg`
`count_mul` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul`	—	`IsDedekindDomain.HeightOneSpectrum.associates_irreducible` `exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain` `Associates.mk_eq_zero` `Ideal.zero_eq_bot` `Ideal.span_singleton_eq_bot` `Associates.mk_ne_zero` `ideal_factor_ne_zero` `IsScalarTower.right` `mul_assoc` `mul_comm` `spanSingleton_mul_spanSingleton` `coeIdeal_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_inv` `Ideal.uniqueFactorizationMonoid` `count_well_defined` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `Associates.count_mul` `IsScalarTower.left` `Ideal.span_singleton_mul_span_singleton` `Ideal.instIsTwoSided_1` `Nat.cast_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt`
`count_mul'` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `instZero`	—	`count_mul` `not_ne_iff` `mul_ne_zero_iff` `IsDomain.to_noZeroDivisors` `instIsDomain` `count_zero`
`count_ne_zero` 📖	mathematical	—	`count` `Associates.count` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `FractionalIdeal` `nonZeroDivisors` `Field.toCommRing` `instMul` `spanSingleton` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `coeIdeal` `exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain` `Ideal.span` `Set` `Set.instSingletonSet`	—	`Ideal.uniqueFactorizationMonoid` `exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain`
`count_neg_zpow` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield`	—	`neg_zero` `zpow_zero` `count_one` `zero_zpow` `neg_ne_zero` `count_zero` `eq_neg_iff_add_eq_zero` `count_mul` `zpow_ne_zero` `zpow_add₀` `neg_add_cancel`
`count_one` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instOne`	—	`RingHom.map_one` `Ideal.one_eq_top` `coeIdeal_top` `mul_one` `inv_one` `spanSingleton_one` `Ideal.uniqueFactorizationMonoid` `count_well_defined` `one_ne_zero` `NeZero.one` `instNontrivialNonZeroDivisors` `Ideal.span_singleton_one` `sub_self`
`count_pow` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instPowNat`	—	`pow_zero` `MulZeroClass.zero_mul` `count_one` `pow_succ` `count_mul'` `le_antisymm` `le_trans` `le_of_eq` `le_refl` `ge_of_eq` `count_zero` `MulZeroClass.mul_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt`
`count_pow_self` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instPowNat` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`count_pow` `count_self` `mul_one`
`count_prod` 📖	mathematical	—	`count` `Finset.prod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `Int.instAddCommMonoid`	—	`Finset.induction` `Finset.prod_empty` `Finset.sum_empty` `count_one` `Finset.mem_insert_of_mem` `Finset.prod_ne_zero_iff` `instNontrivialNonZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Finset.mem_insert_self` `Finset.prod_insert` `Finset.sum_insert` `count_mul`
`count_self` 📖	mathematical	—	`count` `coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`coeIdeal_ne_zero` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `RingHom.map_one` `inv_one` `spanSingleton_one` `one_mul` `IsDedekindDomain.HeightOneSpectrum.associates_irreducible` `Ideal.uniqueFactorizationMonoid` `count_well_defined` `Associates.count_self` `Ideal.instNontrivial` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.span_singleton_one` `Ideal.one_eq_top` `Associates.mk_one` `Associates.factors_one` `Associates.count_zero` `sub_zero`
`count_well_defined` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `spanSingleton` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `coeIdeal`	`count` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Ideal.span` `Set` `Set.instSingletonSet`	—	`exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain` `ideal_factor_ne_zero` `constant_factor_ne_zero` `spanSingleton_eq_zero_iff` `RingHom.map_zero` `IsLocalization.injective` `le_refl` `Ideal.span_singleton_eq_bot` `Ideal.zero_eq_bot` `IsDedekindDomain.HeightOneSpectrum.irreducible` `Ideal.uniqueFactorizationMonoid` `count.eq_1` `sub_eq_sub_iff_add_eq_add` `Associates.count_mul` `Associates.mk_eq_zero` `IsScalarTower.right` `coeIdeal_injective` `coeIdeal_mul` `coeIdeal_span_singleton` `div_eq_div_iff` `div_spanSingleton`
`count_zero` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero`	—	`Ideal.uniqueFactorizationMonoid`
`count_zpow` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield`	—	`zpow_natCast` `count_pow` `count_neg_zpow` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.mul_one`
`count_zpow_self` 📖	mathematical	—	`count` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`count_zpow` `count_self` `mul_one`
`divMod_spec` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instAdd` `instMul` `spanSingleton` `divMod`	—	`divMod.eq_1` `IsDedekindDomain.exists_add_spanSingleton_mul_eq`
`divMod_zero_left` 📖	mathematical	—	`divMod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`divMod_zero_of_not_le` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`divMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`divMod_zero_right` 📖	mathematical	—	`divMod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instCanonicallyOrderedAdd`
`finite_factors` 📖	mathematical	—	`Filter.Eventually` `IsDedekindDomain.HeightOneSpectrum` `count` `Filter.cofinite`	—	`count.congr_simp` `count_zero` `Ideal.uniqueFactorizationMonoid` `exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain` `count_ne_zero` `finite_factors'`
`finite_factors'` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `spanSingleton` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `coeIdeal`	`Filter.Eventually` `IsDedekindDomain.HeightOneSpectrum` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Ideal.span` `Set` `Set.instSingletonSet` `Filter.cofinite`	—	`constant_factor_ne_zero` `ideal_factor_ne_zero` `Ideal.uniqueFactorizationMonoid` `IsScalarTower.right` `IsDedekindDomain.HeightOneSpectrum.irreducible` `sub_self` `Associates.count_ne_zero_iff_dvd` `Set.mem_setOf_eq` `Set.mem_union` `Set.Finite.subset` `Set.Finite.union` `Ideal.finite_factors`
`finprod_heightOneSpectrum_factorization` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `spanSingleton` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `coeIdeal`	`finprod` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `semifield` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Ideal.span` `Set` `Set.instSingletonSet`	—	`ideal_factor_ne_zero` `Ideal.uniqueFactorizationMonoid` `Ideal.finprod_heightOneSpectrum_factorization_coe` `constant_factor_ne_zero` `IsDedekindDomain.toIsDomain` `div_spanSingleton` `div_eq_mul_inv` `coeIdeal_span_singleton` `finprod_inv_distrib` `finprod_mul_distrib` `Ideal.finite_mulSupport_coe` `Ideal.finite_mulSupport_inv` `finprod_congr` `zpow_add₀` `coeIdeal_ne_zero` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `sub_eq_add_neg`
`finprod_heightOneSpectrum_factorization'` 📖	mathematical	—	`finprod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `count`	—	`exists_eq_spanSingleton_mul` `IsDedekindDomain.toIsDomain` `Ideal.uniqueFactorizationMonoid` `finprod_heightOneSpectrum_factorization` `finprod_congr` `count_ne_zero`
`finprod_heightOneSpectrum_factorization_principal` 📖	mathematical	`spanSingleton` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`finprod` `FractionalIdeal` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Ideal.span` `Set` `Set.instSingletonSet` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `IsLocalization.mk'` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalization.exists_mk'_eq` `MonoidWithZero.toMulZeroOneClass`	—	`IsLocalization.exists_mk'_eq` `Ideal.uniqueFactorizationMonoid` `spanSingleton_zero` `zero_div` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.mk'_eq_div` `finprod_heightOneSpectrum_factorization_principal_fraction`
`finprod_heightOneSpectrum_factorization_principal_fraction` 📖	mathematical	—	`finprod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `semifield` `coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Ideal.span` `Set` `Set.instSingletonSet` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `spanSingleton` `IsLocalization.mk'` `Semifield.toCommSemiring` `Field.toSemifield`	—	`map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `spanSingleton_ne_zero_iff` `IsFractionRing.mk'_eq_div` `div_eq_zero_iff` `map_ne_zero_iff` `coeIdeal_span_singleton` `spanSingleton_mul_spanSingleton` `div_eq_mul_inv` `mul_comm` `finprod_heightOneSpectrum_factorization`
`zero_divMod` 📖	mathematical	—	`divMod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instCanonicallyOrderedAdd`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_factors` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `setOf` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`IsScalarTower.right` `Set.finite_coe_iff` `Set.coe_setOf` `Finite.of_injective` `Finite.of_fintype` `uniqueFactorizationMonoid` `Finite.of_subsingleton` `Unique.instSubsingleton` `Preorder.subsingleton_hom` `Subtype.coe_injective` `IsDedekindDomain.HeightOneSpectrum.ext`
`finite_mulSupport` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `Function.mulSupport` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.one` `Semiring.toModule` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing`	—	`Set.Finite.subset` `uniqueFactorizationMonoid` `Filter.eventually_cofinite` `Associates.finite_factors` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing.eq_1` `pow_zero`
`finite_mulSupport_coe` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `Function.mulSupport` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `FractionalIdeal.instOne` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `FractionalIdeal.coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `uniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid` `Function.mulSupport.eq_1` `zpow_natCast` `IsScalarTower.right` `finite_mulSupport`
`finite_mulSupport_inv` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `Function.mulSupport` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `FractionalIdeal.instOne` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `FractionalIdeal.coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `uniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid` `Function.mulSupport.eq_1` `zpow_neg` `finite_mulSupport_coe`
`finprod_count` 📖	mathematical	—	`Associates.count` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.factors` `uniqueFactorizationMonoid` `finprod` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing`	—	`Associates.finprod_ne_zero` `IsDedekindDomain.HeightOneSpectrum.associates_irreducible` `finprod_mem_dvd` `finite_mulSupport` `IsScalarTower.right` `uniqueFactorizationMonoid` `finprod_not_dvd` `Associates.prime_pow_dvd_iff_le` `Associates.mk_pow` `not_le`
`finprod_heightOneSpectrum_factorization` 📖	mathematical	—	`finprod` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing`	—	`associated_iff_eq` `Unique.instSubsingleton` `Associates.mk_eq_mk_iff_associated` `Associates.eq_of_eq_counts` `uniqueFactorizationMonoid` `Associates.finprod_ne_zero` `Associates.mk_ne_zero` `Associates.exists_rep` `finprod_count` `isPrime_of_prime` `irreducible_iff_prime` `isCancelMulZero` `UniqueFactorizationMonoid.instDecompositionMonoid` `Irreducible.ne_zero`
`finprod_heightOneSpectrum_factorization_coe` 📖	mathematical	—	`finprod` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `FractionalIdeal.commSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `FractionalIdeal.coeIdeal` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `Ideal` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `uniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid` `finprod_heightOneSpectrum_factorization` `FractionalIdeal.coeIdeal_finprod` `le_refl` `IsScalarTower.right` `FractionalIdeal.coeIdeal_pow` `zpow_natCast`
`finprod_not_dvd` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.instPowNat` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `Associates.count` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Associated.setoid` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates` `Associates.instCommMonoidWithZero` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Associates.factors` `uniqueFactorizationMonoid` `finprod` `IsDedekindDomain.HeightOneSpectrum` `CommSemiring.toCommMonoid` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing`	—	`finite_mulSupport` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `uniqueFactorizationMonoid` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `IsScalarTower.right` `mul_finprod_cond_ne` `pow_add` `pow_one` `finprod_cond_ne` `prime_of_isPrime` `IsDedekindDomain.HeightOneSpectrum.isPrime` `Prime.exists_mem_finset_dvd` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `isCancelMulZero` `Prime.dvd_of_dvd_pow` `Finset.mem_erase` `IsDedekindDomain.HeightOneSpectrum.ext` `associated_iff_eq` `Unique.instSubsingleton` `Prime.dvd_prime_iff_associated`
`map_algebraMap_eq_finset_prod_pow` 📖	mathematical	—	`map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Finset.prod` `Ideal` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Set.toFinset` `primesOver` `instFintypeElemIdealPrimesOver` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `ramificationIdx`	—	`map_ne_bot_of_ne_bot` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsScalarTower.right` `finprod_heightOneSpectrum_factorization` `finite_factors` `finprod_eq_finset_prod_of_mulSupport_subset` `Set.coe_toFinset` `uniqueFactorizationMonoid` `one_eq_top` `IsScalarTower.left` `IsPrime.ne_top` `IsDedekindDomain.HeightOneSpectrum.isPrime` `Associates.count_ne_zero_iff_dvd` `IsDedekindDomain.HeightOneSpectrum.irreducible` `Finset.prod_set_coe` `Fintype.prod_equiv` `Unique.instSubsingleton` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count` `IsDedekindDomain.ramificationIdx_eq_factors_count` `IsDedekindDomain.HeightOneSpectrum.ne_bot` `Multiset.count.congr_simp` `UniqueFactorizationMonoid.factors_eq_normalizedFactors`

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_add_spanSingleton_mul_eq` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `FractionalIdeal.instPartialOrder`	`FractionalIdeal.instAdd` `FractionalIdeal.instMul` `FractionalIdeal.spanSingleton`	—	`IsScalarTower.right` `FractionalIdeal.coeIdeal_le_coeIdeal` `FractionalIdeal.coeIdeal_mul` `FractionalIdeal.coeIdeal_span_singleton` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `mul_le_mul_right` `FractionalIdeal.instMulLeftMono` `exists_sup_span_eq` `IsScalarTower.left` `IsDomain.to_noZeroDivisors` `toIsDomain` `IsDomain.toNontrivial` `Iff.not` `FractionalIdeal.num_eq_zero_iff` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `FractionalIdeal.spanSingleton.congr_simp` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsFractionRing.instFaithfulSMul` `add_mul` `Distrib.rightDistribClass` `FractionalIdeal.spanSingleton_mul_spanSingleton` `IsUnit.div_mul_cancel` `mul_assoc` `mul_comm` `FractionalIdeal.den_mul_self_eq_num'` `mul_right_comm` `one_ne_zero` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `mul_add` `Distrib.leftDistribClass` `mul_inv_cancel_left₀`
`exists_eq_span_pair` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal.span` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`exists_sup_span_eq` `Ideal.span_singleton_le_iff_mem` `Set.union_singleton` `Set.pair_comm`
`exists_sup_span_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `Ideal.dvd_iff_le` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `toIsDomain` `Ideal.finite_factors` `mul_one` `Finset.prod_eq_mul_prod_diff_singleton` `mul_assoc` `mul_right_comm` `mul_lt_mul_of_pos_left` `instPosMulStrictMonoIdeal` `Ideal.one_eq_top` `lt_top_iff_ne_top` `Ideal.IsPrime.ne_top` `HeightOneSpectrum.isPrime` `Ideal.zero_eq_bot` `bot_lt_iff_ne_bot` `mul_ne_zero_iff` `Finset.prod_ne_zero_iff` `Ideal.instNontrivial` `IsDomain.toNontrivial` `HeightOneSpectrum.ne_bot` `Ideal.span_singleton_le_iff_mem` `sum_mem` `Submodule.addSubmonoidClass` `Ideal.mul_le_right` `Ideal.instIsTwoSided_1` `Ideal.exists_le_maximal` `Ideal.IsMaximal.isPrime` `Set.Finite.toFinset.congr_simp` `LE.le.trans` `le_sup_left` `Ideal.mul_mono_right` `le_sup_right` `Eq.trans_le` `Ideal.mem_span_singleton_self` `Ideal.prod_le_inf` `Finset.inf_le` `Finset.mem_singleton` `Finset.mem_sdiff` `inf_prime_pow_eq_prod` `HeightOneSpectrum.prime` `HeightOneSpectrum.ext` `pow_one` `Finset.prod_congr` `Finset.inf_eq_iInf` `iInf_subtype'` `Ideal.mul_iInf` `Ideal.mem_iInf` `Finset.sum_eq_add_sum_diff_singleton` `add_sub_cancel_right` `sub_mem` `Submodule.addSubgroupClass` `Nontrivial.to_nonempty` `SetLike.exists_of_lt` `instIsConcreteLE` `Function.sometimes_spec` `Ideal.add_eq_sup` `mul_add` `Distrib.leftDistribClass` `IsScalarTower.left` `Ideal.mul_top`

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
`maxPowDividing` 📖	CompOp	6 math math: `Ideal.finite_mulSupport`, `Ideal.finprod_count`, `maxPowDividing_eq_pow_multiset_count`, `embedding_mul_absNorm`, `Ideal.finprod_not_dvd`, `Ideal.finprod_heightOneSpectrum_factorization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`maxPowDividing_eq_pow_multiset_count` 📖	mathematical	—	`maxPowDividing` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `asIdeal` `Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	—	`IsScalarTower.right` `Ideal.uniqueFactorizationMonoid` `maxPowDividing.eq_1` `irreducible` `Associates.count_some` `Multiset.count_map_eq_count'` `Subtype.val_injective` `Associates.map_subtype_coe_factors'` `Unique.instSubsingleton` `UniqueFactorizationMonoid.factors_eq_normalizedFactors` `Associates.mk_injective`

---

← Back to Index