Lemmas

📁 Source: Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Statistics

Metric	Count
Definitions `instNormalizedGCDMonoid`, `asIdeal`, `equivMaximalSpectrum`, `equivPrimesOver`, `ofPrime`, `quotientEquivPiFactors`, `quotientEquivPiOfFinsetProdEq`, `quotientEquivPiOfProdEq`, `idealFactorsEquivOfQuotEquiv`, `idealFactorsFunOfQuotHom`, `instFintypeElemIdealPrimesOver`, `normalizedFactorsEquivOfQuotEquiv`, `normalizedFactorsEquivSpanNormalizedFactors`, `primesOverFinset`	14
Theorems `le_singleton_iff`, `exists_notMem_one_of_ne_bot`, `inf_mul`, `inv_le_comm`, `inv_le_inv_iff`, `le_inv_comm`, `mul_inf`, `sup_mul_inf`, `mem_pow_mul`, `mul_mem_pow`, `count_associates_eq`, `count_associates_eq'`, `count_normalizedFactors_eq`, `dvd_span_singleton`, `eq_prime_pow_mul_coprime`, `eq_prime_pow_of_succ_lt_of_le`, `exist_integer_multiples_notMem`, `exists_mem_pow_notMem_pow_succ`, `factors_span_eq`, `gcd_eq_sup`, `iInf_mul`, `inf_mul`, `isCoprime_iff_gcd`, `isPrime_iff_bot_or_prime`, `isPrime_of_prime`, `lcm_eq_inf`, `le_mul_of_no_prime_factors`, `mem_normalizedFactors_iff`, `mem_primesOver_iff_mem_normalizedFactors`, `mul_iInf`, `mul_inf`, `pow_lt_self`, `pow_right_strictAnti`, `pow_succ_lt_pow`, `prime_generator_of_prime`, `prime_iff_isPrime`, `prime_of_isPrime`, `prime_of_mem_primesOver`, `prime_span_singleton_iff`, `squarefree_span_singleton`, `sup_mul_inf`, `associates_irreducible`, `equivPrimesOver_apply`, `ext`, `ext_iff`, `iInf_localization_eq_bot`, `ideal_ne_top_iff_exists`, `irreducible`, `isMaximal`, `isPrime`, `ne_bot`, `ofPrime_asIdeal`, `prime`, `exists_forall_sub_mem_ideal`, `exists_representative_mod_finset`, `inf_prime_pow_eq_prod`, `quotientEquivPiFactors_mk`, `primesOverFinset_eq`, `prime_le_prime_iff_eq`, `coe_primesOverFinset`, `count_associates_factors_eq`, `count_le_of_ideal_ge`, `count_span_normalizedFactors_eq`, `count_span_normalizedFactors_eq_of_normUnit`, `emultiplicity_eq_emultiplicity_span`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity`, `idealFactorsEquivOfQuotEquiv_is_dvd_iso`, `idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors`, `idealFactorsEquivOfQuotEquiv_symm`, `idealFactorsFunOfQuotHom_coe_coe`, `idealFactorsFunOfQuotHom_comp`, `idealFactorsFunOfQuotHom_id`, `irreducible_pow_sup`, `irreducible_pow_sup_of_ge`, `irreducible_pow_sup_of_le`, `map_prime_of_equiv`, `mem_primesOverFinset_iff`, `normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity`, `normalizedFactorsEquivOfQuotEquiv_symm`, `one_le_primesOver_ncard`, `primesOver_finite`, `primesOver_ncard_ne_zero`, `prod_normalizedFactors_eq_self`, `singleton_span_mem_normalizedFactors_of_mem_normalizedFactors`, `span_singleton_dvd_span_singleton_iff_dvd`, `sup_eq_prod_inf_factors`	87
Total	101

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_singleton_iff` 📖	mathematical	—	`Associates` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Preorder.toLE` `instPreorder` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Monoid.toNatPow` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `Ideal.span` `Set` `Set.instSingletonSet` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right`	—	`IsScalarTower.right`

FractionalIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_notMem_one_of_ne_bot` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `instSetLike` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `coeIdeal` `instOne`	—	`IsDedekindDomain.toIsDomain` `Set.not_subset` `not_inv_le_one_of_ne_bot`
`inf_mul` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `instMin`	—	`inf_mul₀` `MulPosReflectLE.toMulPosReflectLT` `instMulPosReflectLENonZeroDivisors` `zero_le`
`inv_le_comm` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain`	—	`IsDedekindDomain.toIsDomain` `inv_inv` `le_inv_comm` `inv_ne_zero`
`inv_le_inv_iff` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain`	—	`IsDedekindDomain.toIsDomain` `le_inv_comm` `inv_ne_zero` `inv_inv`
`le_inv_comm` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain`	—	`IsDedekindDomain.toIsDomain` `inv_eq` `le_div_iff_mul_le` `mul_comm`
`mul_inf` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `instMin`	—	`mul_inf₀` `PosMulReflectLE.toPosMulReflectLT` `instPosMulReflectLENonZeroDivisors` `zero_le`
`sup_mul_inf` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `instMin` `instMax`	—	`mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `spanSingleton.congr_simp` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsDomain.to_noZeroDivisors` `IsFractionRing.instFaithfulSMul` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsScalarTower.right` `Ideal.sup_mul_inf` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `mul_inf₀` `PosMulReflectLE.toPosMulReflectLT` `instPosMulReflectLENonZeroDivisors` `zero_le` `mul_add` `Distrib.leftDistribClass` `mul_left_comm` `coeIdeal_mul` `coeIdeal_sup` `coeIdeal_span_singleton` `coeIdeal_inf` `Module.IsTorsionFree.to_faithfulSMul` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree`

Ideal

Definitions

Name	Category	Theorems
`instNormalizedGCDMonoid` 📖	CompOp	3 math math: `gcd_eq_sup`, `isCoprime_iff_gcd`, `lcm_eq_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_associates_eq` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Associates.count` `Ideal` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `span` `Set` `Set.instSingletonSet` `Associates.factors` `uniqueFactorizationMonoid`	—	`Prime.ne_zero` `uniqueFactorizationMonoid` `count_associates_factors_eq` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `isReduced_of_noZeroDivisors` `IsDomain.toNontrivial` `span_singleton_prime` `UniqueFactorizationMonoid.count_normalizedFactors_eq` `Prime.irreducible` `isCancelMulZero` `prime_span_singleton_iff` `normalize_eq` `span_singleton_pow` `instIsTwoSided_1` `mul_mem_right` `mem_span_singleton_self` `pow_add` `pow_one` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `pow_ne_zero`
`count_associates_eq'` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Associates.count` `Ideal` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `span` `Set` `Set.instSingletonSet` `Associates.factors` `uniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid` `count_associates_eq` `Mathlib.Tactic.Contrapose.contrapose₄` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast`
`count_normalizedFactors_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	`Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `normalizationMonoid` `uniqueFactorizationMonoid`	—	`IsScalarTower.right` `UniqueFactorizationMonoid.count_normalizedFactors_eq'` `uniqueFactorizationMonoid` `Unique.instSubsingleton` `Prime.irreducible` `isCancelMulZero` `isPrime_iff_bot_or_prime` `normalize_eq` `dvd_iff_le` `le_of_dvd`
`dvd_span_singleton` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `span` `Set` `Set.instSingletonSet` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `dvd_iff_le` `span_le` `Set.singleton_subset_iff`
`eq_prime_pow_mul_coprime` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `Submodule.instPowNat` `Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `normalizationMonoid` `uniqueFactorizationMonoid`	—	`IsScalarTower.right` `uniqueFactorizationMonoid` `sup_multiset_prod_eq_top` `UniqueFactorizationMonoid.prime_of_normalized_factor` `Multiset.filter_subset` `IsMaximal.coprime_of_ne` `IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsDedekindDomain.toIsDedekindRing` `isPrime_of_prime` `Prime.ne_zero` `Multiset.of_mem_filter` `prod_normalizedFactors_eq_self` `Multiset.filter_add_not` `Multiset.prod_add` `Multiset.pow_count`
`eq_prime_pow_of_succ_lt_of_le` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Preorder.toLE`	—	—	`IsScalarTower.right` `le_antisymm` `prime_of_isPrime` `LT.lt.ne'` `lt_of_le_of_lt` `bot_le` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `dvd_iff_le` `uniqueFactorizationMonoid` `UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors` `UniqueFactorizationMonoid.normalizedFactors_pow` `UniqueFactorizationMonoid.normalizedFactors_irreducible` `Prime.irreducible` `isCancelMulZero` `Multiset.nsmul_singleton` `Multiset.lt_replicate_succ` `UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors` `dvdNotUnit_iff_lt`
`exist_integer_multiples_notMem` 📖	mathematical	`Finset` `Finset.instMembership`	`IsLocalization.IsInteger` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `FractionalIdeal.instSetLike` `FractionalIdeal.coeIdeal`	—	`FractionalIdeal.spanFinset_ne_zero` `IsDedekindDomain.toIsDomain` `div_eq_mul_inv` `mul_lt_of_lt_one_left` `FractionalIdeal.instMulPosStrictMonoNonZeroDivisors` `FractionalIdeal.instCanonicallyOrderedAdd` `FractionalIdeal.coeIdeal_top` `strictMono_of_le_iff_le` `FractionalIdeal.coeIdeal_le_coeIdeal` `lt_top_iff_ne_top` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `FractionalIdeal.mem_one_iff` `FractionalIdeal.mem_inv_iff` `Submodule.subset_span` `Set.mem_image_of_mem` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `FractionalIdeal.mem_div_iff_of_ne_zero` `Submodule.span_induction` `MulZeroClass.mul_zero` `Submodule.zero_mem` `mul_add` `Distrib.leftDistribClass` `Submodule.add_mem` `mul_smul_comm` `Algebra.to_smulCommClass` `Submodule.smul_mem`
`exists_mem_pow_notMem_pow_succ` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`SetLike.exists_of_lt` `instIsConcreteLE` `IsScalarTower.right` `pow_right_strictAnti`
`factors_span_eq` 📖	mathematical	—	`UniqueFactorizationMonoid.factors` `Ideal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.semiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Polynomial.commSemiring` `Semifield.toCommSemiring` `uniqueFactorizationMonoid` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `span` `Set` `Set.instSingletonSet` `Multiset.map` `PrincipalIdealRing.to_uniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `eq_or_ne` `Unique.instSubsingleton` `UniqueFactorizationMonoid.factors.congr_simp` `span_zero` `UniqueFactorizationMonoid.factors_eq_normalizedFactors` `Multiset.map_congr` `UniqueFactorizationMonoid.factors_zero` `UniqueFactorizationMonoid.normalizedFactors_zero` `Multiset.mem_map` `prime_span_singleton_iff` `UniqueFactorizationMonoid.prime_of_factor` `span_singleton_eq_span_singleton` `UniqueFactorizationMonoid.factors_prod` `multiset_prod_span_singleton` `UniqueFactorizationMonoid.normalizedFactors_prod_of_prime`
`gcd_eq_sup` 📖	mathematical	—	`GCDMonoid.gcd` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `NormalizedGCDMonoid.toGCDMonoid` `instNormalizedGCDMonoid` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id`	—	—
`iInf_mul` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `iInf` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `mul_comm` `mul_iInf`
`inf_mul` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `mul_comm` `mul_inf`
`isCoprime_iff_gcd` 📖	mathematical	—	`IsCoprime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `NormalizedGCDMonoid.toGCDMonoid` `instNormalizedGCDMonoid` `Submodule.one` `Semiring.toModule`	—	`isCoprime_iff_codisjoint` `codisjoint_iff` `one_eq_top` `gcd_eq_sup`
`isPrime_iff_bot_or_prime` 📖	mathematical	—	`IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Prime` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	—	`prime_of_isPrime` `eq_or_ne` `isPrime_bot` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `isPrime_of_prime`
`isPrime_of_prime` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	`IsPrime`	—	`Prime.not_unit` `one_eq_top` `isUnit_one` `IsScalarTower.right` `Prime.dvd_or_dvd` `IsScalarTower.left` `instIsTwoSided_1`
`lcm_eq_inf` 📖	mathematical	—	`GCDMonoid.lcm` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `NormalizedGCDMonoid.toGCDMonoid` `instNormalizedGCDMonoid` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`le_mul_of_no_prime_factors` 📖	mathematical	`IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Submodule.mul` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `MulZeroClass.zero_mul` `mul_comm` `mul_dvd_mul_left` `UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors` `uniqueFactorizationMonoid` `isPrime_of_prime`
`mem_normalizedFactors_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `normalizationMonoid` `uniqueFactorizationMonoid` `IsPrime` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`uniqueFactorizationMonoid` `IsScalarTower.right` `dvd_iff_le` `zero_eq_bot` `UniqueFactorizationMonoid.mem_normalizedFactors_iff` `Unique.instSubsingleton` `prime_iff_isPrime`
`mem_primesOver_iff_mem_normalizedFactors` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `primesOver` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `normalizationMonoid` `uniqueFactorizationMonoid` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`uniqueFactorizationMonoid` `primesOver.eq_1` `Set.mem_setOf_eq` `mem_normalizedFactors_iff` `map_ne_bot_of_ne_bot` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `liesOver_iff` `RingHom.instRingHomClass` `under_def` `map_le_iff_le_comap` `le_of_eq` `IsCoatom.le_iff_eq` `isMaximal_def` `comap_ne_top` `IsPrime.ne_top`
`mul_iInf` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `iInf` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `Submodule.bot_mul` `ciInf_const` `LE.le.antisymm` `IsScalarTower.left` `le_iInf` `mul_mono_right` `iInf_le` `LE.le.trans` `mul_le_right` `instIsTwoSided_1` `dvd_iff_le` `le_imp_le_of_le_of_le` `mul_le_mul_right` `Submodule.instMulLeftMono` `mul_le_mul_iff_of_pos_left` `IsOrderedRing.toPosMulMono` `Submodule.instIsOrderedRing` `FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain` `bot_lt_iff_ne_bot` `le_refl`
`mul_inf` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `inf_eq_iInf` `mul_iInf`
`pow_lt_self` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `pow_one` `pow_right_strictAnti`
`pow_right_strictAnti` 📖	mathematical	—	`StrictAnti` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`strictAnti_nat_of_succ_lt` `IsScalarTower.right` `dvdNotUnit_iff_lt` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `isUnit_iff` `pow_succ`
`pow_succ_lt_pow` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`lt_of_le_of_ne` `IsScalarTower.right` `pow_le_pow_right` `pow_inj_of_not_isUnit` `isCancelMulZero` `isUnit_iff` `IsPrime.ne_top`
`prime_generator_of_prime` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	`Submodule.IsPrincipal.generator` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`isPrime_of_prime` `Submodule.IsPrincipal.prime_generator_of_isPrime` `Prime.ne_zero`
`prime_iff_isPrime` 📖	mathematical	—	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `IsPrime`	—	`isPrime_of_prime` `prime_of_isPrime`
`prime_of_isPrime` 📖	mathematical	—	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	—	`isUnit_iff` `IsPrime.ne_top` `IsScalarTower.right` `IsPrime.mul_le` `le_of_dvd`
`prime_of_mem_primesOver` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `primesOver`	`Prime` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	—	`prime_of_isPrime` `ne_bot_of_mem_primesOver` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain`
`prime_span_singleton_iff` 📖	mathematical	—	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `span` `Set` `Set.instSingletonSet`	—	`eq_or_ne` `Set.singleton_zero` `span_zero` `zero_eq_bot` `not_iff_not` `prime_iff_isPrime` `span_singleton_prime`
`squarefree_span_singleton` 📖	mathematical	—	`Squarefree` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `span` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `IsScalarTower.left` `span_singleton_mul_span_singleton` `instIsTwoSided_1` `span_singleton_dvd_span_singleton_iff_dvd` `isUnit_iff` `eq_top_of_isUnit_mem` `IsPrincipalIdealRing.principal` `Submodule.IsPrincipal.generator_mem` `span_singleton_generator`
`sup_mul_inf` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`uniqueFactorizationMonoid` `gcd_eq_normalize` `IsScalarTower.right` `dvd_iff_le` `sup_le_iff` `GCDMonoid.gcd_dvd_left` `GCDMonoid.gcd_dvd_right` `dvd_gcd_iff` `Unique.instSubsingleton` `normalize_eq` `lcm_eq_normalize` `lcm_dvd_iff` `le_inf_iff` `dvd_lcm_left` `dvd_lcm_right` `associated_iff_eq` `gcd_mul_lcm`

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_pow_mul` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`IsScalarTower.right` `mul_mem_pow` `mul_comm`
`mul_mem_pow` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`IsScalarTower.right` `pow_zero` `Ideal.one_eq_top` `pow_succ` `Submodule.mul_bot` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Prime.pow_dvd_of_dvd_mul_right` `Ideal.isCancelMulZero` `Ideal.prime_iff_isPrime` `mul_comm` `IsScalarTower.left` `Ideal.instIsTwoSided_1`

IsDedekindDomain

Definitions

Name	Category	Theorems
`quotientEquivPiFactors` 📖	CompOp	1 math math: `quotientEquivPiFactors_mk`
`quotientEquivPiOfFinsetProdEq` 📖	CompOp	—
`quotientEquivPiOfProdEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_forall_sub_mem_ideal` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring`	`SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset` `Finset.instSetLike`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `exists_representative_mod_finset` `Ideal.Quotient.eq`
`exists_representative_mod_finset` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `RingEquiv.surjective` `Ideal.Quotient.mk_surjective`
`inf_prime_pow_eq_prod` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring`	`Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instOrderTop` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.induction` `IsScalarTower.right` `instIsEmptyFalse` `Ideal.one_eq_top` `Finset.inf_insert` `Finset.prod_insert` `Finset.mem_insert_of_mem` `le_antisymm` `Ideal.le_mul_of_no_prime_factors` `Ideal.IsPrime.prod_le` `Finset.mem_insert_self` `Ring.DimensionLeOne.prime_le_prime_iff_eq` `IsDedekindRing.toDimensionLEOne` `toIsDedekindRing` `Ideal.isPrime_of_prime` `Prime.ne_zero` `Ideal.IsPrime.le_of_pow_le` `inf_le_left` `inf_le_right` `Ideal.mul_le_inf` `Ideal.instIsTwoSided_1`
`quotientEquivPiFactors_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `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` `Multiset.count` `Distrib.toAdd` `Pi.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientEquivPiFactors` `RingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.uniqueFactorizationMonoid` `IsScalarTower.right` `Ideal.instIsTwoSided_1`

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
`asIdeal` 📖	CompOp	61 math math: `equivPrimesOver_apply`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal`, `iInf_localization_eq_bot`, `NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal`, `Polynomial.idealX_span`, `Associates.finite_factors`, `NumberField.FinitePlace.norm_def'`, `isMaximal`, `intValuation_if_neg`, `FractionalIdeal.count_well_defined`, `FractionalIdeal.count_finsuppProd`, `intValuationDef_if_neg`, `intValuation_le_pow_iff_mem`, `FractionalIdeal.count_finprod_coprime`, `ofPrime_asIdeal`, `FractionalIdeal.finprod_heightOneSpectrum_factorization`, `irreducible`, `intValuation_le_pow_iff_dvd`, `FractionalIdeal.count_finprod`, `FractionalIdeal.count_ne_zero`, `Polynomial.gaussNorm_lt_one_iff_contentIdeal_le`, `valuation_lt_one_iff_dvd`, `NumberField.FinitePlace.norm_lt_one_iff_mem`, `Rat.valuation_le_one_iff_den`, `ext_iff`, `intAdicAbv_lt_one_iff`, `FractionalIdeal.count_maximal_coprime`, `prime`, `valuation_lt_one_iff_mem`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `Rat.HeightOneSpectrum.natGenerator_dvd_iff`, `NumberField.FinitePlace.norm_def_int`, `intValuation_lt_one_iff_dvd`, `Ideal.finite_mulSupport_coe`, `Rat.HeightOneSpectrum.span_natGenerator`, `intValuation_eq_one_iff`, `intAdicAbv_eq_one_iff`, `FractionalIdeal.count_zpow_self`, `intValuation_def`, `Ideal.finite_factors`, `NumberField.FinitePlace.norm_eq_one_iff_notMem`, `Ideal.finprod_count`, `maxPowDividing_eq_pow_multiset_count`, `FractionalIdeal.count_pow_self`, `NumberField.toNNReal_valued_eq_adicAbv`, `Ideal.finprod_heightOneSpectrum_factorization_coe`, `FractionalIdeal.finite_factors'`, `FractionalIdeal.count_self`, `isPrime`, `FractionalIdeal.count_maximal`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction`, `NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm`, `Ideal.finprod_not_dvd`, `associates_irreducible`, `Ideal.finite_mulSupport_inv`, `adicAbv_coe_eq_one_iff`, `ideal_ne_top_iff_exists`, `adicAbv_coe_lt_one_iff`, `FractionalIdeal.count_coe`, `intValuation_lt_one_iff_mem`, `FractionalIdeal.finprod_heightOneSpectrum_factorization'`
`equivMaximalSpectrum` 📖	CompOp	—
`equivPrimesOver` 📖	CompOp	1 math math: `equivPrimesOver_apply`
`ofPrime` 📖	CompOp	1 math math: `ofPrime_asIdeal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associates_irreducible` 📖	mathematical	—	`Irreducible` `Associates` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `CommMonoidWithZero.toMonoidWithZero` `Associates.instCommMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `asIdeal`	—	`irreducible`
`equivPrimesOver_apply` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Ideal.primesOver` `DFunLike.coe` `Equiv` `IsDedekindDomain.HeightOneSpectrum` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `asIdeal` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivPrimesOver`	—	`IsScalarTower.right`
`ext` 📖	—	`asIdeal`	—	—	—
`ext_iff` 📖	mathematical	—	`asIdeal`	—	`ext`
`iInf_localization_eq_bot` 📖	mathematical	—	`iInf` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsDedekindDomain.HeightOneSpectrum` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Localization.subalgebra.ofField` `Ideal.primeCompl` `CommSemiring.toSemiring` `asIdeal` `isPrime` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Subalgebra.ext` `isPrime` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Algebra.mem_iInf` `Function.bijective_iff_has_inverse` `IsField.localization_map_bijective` `nonZeroDivisors.ne_zero` `IsDomain.toNontrivial` `Algebra.mem_bot` `Ideal.IsMaximal.isPrime'` `MaximalSpectrum.isMaximal` `MaximalSpectrum.iInf_localization_eq_bot` `Ideal.IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsDedekindDomain.toIsDedekindRing`
`ideal_ne_top_iff_exists` 📖	mathematical	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal`	—	`Ideal.ne_top_iff_exists_maximal` `MaximalSpectrum.isMaximal`
`irreducible` 📖	mathematical	—	`Irreducible` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `asIdeal`	—	`UniqueFactorizationMonoid.irreducible_iff_prime` `Ideal.uniqueFactorizationMonoid` `prime`
`isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `asIdeal`	—	`Ideal.IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsDedekindDomain.toIsDedekindRing` `isPrime` `ne_bot`
`isPrime` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `asIdeal`	—	—
`ne_bot` 📖	—	—	—	—	—
`ofPrime_asIdeal` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring`	`asIdeal` `ofPrime`	—	—
`prime` 📖	mathematical	—	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `asIdeal`	—	`Ideal.prime_of_isPrime` `ne_bot` `isPrime`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primesOverFinset_eq` 📖	mathematical	—	`primesOverFinset` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset` `Finset.instSingleton` `maximalIdeal`	—	`IsDomain.of_faithfulSMul` `Finset.coe_eq_singleton` `coe_primesOverFinset` `FaithfulSMul.to_isTorsionFree` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero` `primesOver_eq`

Ring.DimensionLeOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prime_le_prime_iff_eq` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.IsMaximal.eq_of_le` `Ideal.IsPrime.isMaximal` `Ideal.IsPrime.ne_top` `Eq.le`

(root)

Definitions

Name	Category	Theorems
`idealFactorsEquivOfQuotEquiv` 📖	CompOp	3 math math: `idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors`, `idealFactorsEquivOfQuotEquiv_symm`, `idealFactorsEquivOfQuotEquiv_is_dvd_iso`
`idealFactorsFunOfQuotHom` 📖	CompOp	3 math math: `idealFactorsFunOfQuotHom_comp`, `idealFactorsFunOfQuotHom_id`, `idealFactorsFunOfQuotHom_coe_coe`
`instFintypeElemIdealPrimesOver` 📖	CompOp	1 math math: `Ideal.map_algebraMap_eq_finset_prod_pow`
`normalizedFactorsEquivOfQuotEquiv` 📖	CompOp	2 math math: `normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity`, `normalizedFactorsEquivOfQuotEquiv_symm`
`normalizedFactorsEquivSpanNormalizedFactors` 📖	CompOp	2 math math: `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity`
`primesOverFinset` 📖	CompOp	5 math math: `coe_primesOverFinset`, `Ideal.sum_ramification_inertia`, `Ideal.card_primesOverFinset_le_finrank`, `mem_primesOverFinset_iff`, `IsLocalRing.primesOverFinset_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_primesOverFinset` 📖	mathematical	—	`SetLike.coe` `Finset` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset.instSetLike` `primesOverFinset` `Ideal.primesOver`	—	`Set.ext` `Unique.instSubsingleton` `Ideal.uniqueFactorizationMonoid` `UniqueFactorizationMonoid.factors_eq_normalizedFactors` `Ideal.mem_primesOver_iff_mem_normalizedFactors`
`count_associates_factors_eq` 📖	mathematical	—	`Associates.count` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `Ideal.normalizationMonoid`	—	`Associates.mk_ne_zero` `Prime.irreducible` `Ideal.isCancelMulZero` `Ideal.prime_of_isPrime` `Ideal.uniqueFactorizationMonoid` `Ideal.count_normalizedFactors_eq` `IsScalarTower.right` `Ideal.dvd_iff_le` `Associates.mk_pow` `Associates.prime_pow_dvd_iff_le` `le_refl`
`count_le_of_ideal_ge` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	—	`Ideal.uniqueFactorizationMonoid` `Multiset.le_iff_count` `UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors` `ne_bot_of_le_ne_bot` `IsScalarTower.right` `Ideal.dvd_iff_le`
`count_span_normalizedFactors_eq` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	`Multiset.count` `Ideal` `CommSemiring.toSemiring` `Ideal.span` `Set` `Set.instSingletonSet` `UniqueFactorizationMonoid.normalizedFactors` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `PrincipalIdealRing.to_uniqueFactorizationMonoid`	—	`emultiplicity_eq_emultiplicity_span` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `IsScalarTower.left` `Ideal.mul_top` `Ideal.instIsTwoSided_1` `Ideal.one_eq_top` `Units.val_one` `normUnit_eq_one` `normalize_apply` `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors` `Prime.irreducible` `Ideal.isCancelMulZero` `IsDomain.toIsCancelMulZero`
`count_span_normalizedFactors_eq_of_normUnit` 📖	mathematical	`NormalizationMonoid.normUnit` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Units.instOne` `Prime`	`Multiset.count` `Ideal` `CommSemiring.toSemiring` `Ideal.span` `Set` `Set.instSingletonSet` `UniqueFactorizationMonoid.normalizedFactors` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid`	—	`Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Multiset.count.congr_simp` `mul_one` `count_span_normalizedFactors_eq`
`emultiplicity_eq_emultiplicity_span` 📖	mathematical	—	`emultiplicity` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet`	—	`FiniteMultiplicity.emultiplicity_eq_multiplicity` `emultiplicity_eq_of_dvd_of_not_dvd` `IsScalarTower.left` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `span_singleton_dvd_span_singleton_iff_dvd` `pow_multiplicity_dvd` `FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `FiniteMultiplicity.not_iff_forall` `emultiplicity_eq_top`
`emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity` 📖	mathematical	`Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `PrincipalIdealRing.to_uniqueFactorizationMonoid`	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Set` `Set.instMembership` `setOf` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Ideal.span` `Set.instSingletonSet` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `normalizedFactorsEquivSpanNormalizedFactors`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `emultiplicity_eq_emultiplicity_span`
`emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity` 📖	mathematical	—	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `setOf` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `DFunLike.coe` `Equiv` `Set.Elem` `Ideal` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Ideal.span` `Set.instSingletonSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `normalizedFactorsEquivSpanNormalizedFactors` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	`Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Equiv.surjective` `Equiv.symm_apply_apply` `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity`
`idealFactorsEquivOfQuotEquiv_is_dvd_iso` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	`Set` `Set.instMembership` `setOf` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLikeOrderIso` `idealFactorsEquivOfQuotEquiv`	—	`IsScalarTower.right` `OrderIso.le_iff_le` `Ideal.dvd_iff_le` `Subtype.coe_le_coe`
`idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	`Set` `Set.instMembership` `setOf` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLikeOrderIso` `idealFactorsEquivOfQuotEquiv` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors`	—	`Ideal.uniqueFactorizationMonoid` `Finset.notMem_empty` `Multiset.empty_eq_zero` `UniqueFactorizationMonoid.normalizedFactors_zero` `bot_eq_zero` `Submodule.instCanonicallyOrderedAdd` `mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors` `Ideal.isCancelMulZero` `Unique.instSubsingleton` `IsScalarTower.right` `idealFactorsEquivOfQuotEquiv_is_dvd_iso`
`idealFactorsEquivOfQuotEquiv_symm` 📖	mathematical	—	`OrderIso.symm` `Set.Elem` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Set` `Set.instMembership` `idealFactorsEquivOfQuotEquiv` `RingEquiv.symm` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd`	—	`IsScalarTower.right`
`idealFactorsFunOfQuotHom_coe_coe` 📖	mathematical	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.semiring` `RingHom.instFunLike`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `OrderHom` `IsScalarTower.right` `Algebra.id` `Subtype.preorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `OrderHom.instFunLike` `idealFactorsFunOfQuotHom` `Ideal.comap` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.map`	—	`IsScalarTower.right`
`idealFactorsFunOfQuotHom_comp` 📖	mathematical	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.semiring` `RingHom.instFunLike`	`OrderHom.comp` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Subtype.preorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `idealFactorsFunOfQuotHom` `RingHom.comp`	—	`OrderHom.ext` `IsScalarTower.right` `Ideal.instIsTwoSided_1` `idealFactorsFunOfQuotHom.eq_1` `OrderHom.comp_coe` `RingHom.instRingHomClass` `Ideal.map_comap_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.map_map`
`idealFactorsFunOfQuotHom_id` 📖	mathematical	—	`idealFactorsFunOfQuotHom` `RingHom.id` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Semiring.toNonAssocSemiring` `Ideal.Quotient.semiring` `RingHom.surjective` `RingHomSurjective.ids` `OrderHom.id` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Subtype.preorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`OrderHom.ext` `IsScalarTower.right` `RingHom.surjective` `RingHomSurjective.ids` `Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.comap.congr_simp` `Ideal.map_id` `Ideal.comap_map_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.mk_ker` `sup_eq_left` `Ideal.dvd_iff_le` `Subtype.prop` `Subtype.coe_eta`
`irreducible_pow_sup` 📖	mathematical	`Irreducible` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	`SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Multiset.count` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	—	`IsScalarTower.right` `Ideal.uniqueFactorizationMonoid` `sup_eq_prod_inf_factors` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Irreducible.ne_zero` `min_comm` `UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow` `Unique.instSubsingleton` `normalize_eq` `Multiset.replicate_inter` `Multiset.prod_replicate`
`irreducible_pow_sup_of_ge` 📖	mathematical	`Irreducible` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	`SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `multiplicity`	—	`IsScalarTower.right` `Ideal.uniqueFactorizationMonoid` `irreducible_pow_sup` `min_eq_left` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Unique.instSubsingleton` `normalize_eq` `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors` `FiniteMultiplicity.emultiplicity_eq_multiplicity` `emultiplicity_lt_top` `LE.le.trans_lt`
`irreducible_pow_sup_of_le` 📖	mathematical	`Irreducible` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	`SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right`	—	`IsScalarTower.right` `sup_of_le_left` `Ideal.uniqueFactorizationMonoid` `irreducible_pow_sup` `min_eq_right` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Unique.instSubsingleton` `normalize_eq` `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors`
`map_prime_of_equiv` 📖	mathematical	`Prime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring`	`Ideal.map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike`	—	`Ideal.prime_iff_isPrime` `Iff.not` `Ideal.map_eq_bot_iff_of_injective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.injective` `Ideal.map_isPrime_of_equiv`
`mem_primesOverFinset_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset` `Finset.instMembership` `primesOverFinset` `Set` `Set.instMembership` `Ideal.primesOver`	—	`Finset.mem_coe` `coe_primesOverFinset`
`normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Set` `Set.instMembership` `setOf` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `normalizedFactorsEquivOfQuotEquiv`	—	`Ideal.uniqueFactorizationMonoid` `normalizedFactorsEquivOfQuotEquiv.eq_1` `emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors` `Ideal.isCancelMulZero` `Unique.instSubsingleton` `IsScalarTower.right` `idealFactorsEquivOfQuotEquiv_is_dvd_iso`
`normalizedFactorsEquivOfQuotEquiv_symm` 📖	mathematical	—	`Equiv.symm` `Set.Elem` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `normalizedFactorsEquivOfQuotEquiv` `RingEquiv.symm` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd`	—	`Ideal.uniqueFactorizationMonoid`
`one_le_primesOver_ncard` 📖	mathematical	—	`Set.ncard` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver`	—	`primesOver_ncard_ne_zero`
`primesOver_finite` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver`	—	`Ideal.primesOver_bot` `IsDomain.of_bot_isPrime` `Ideal.isPrime_bot` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Set.finite_singleton` `coe_primesOverFinset` `Finset.finite_toSet`
`primesOver_ncard_ne_zero` 📖	—	—	—	—	`Ideal.exists_maximal_ideal_liesOver_of_isIntegral` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Set.ncard_ne_zero_of_mem` `Ideal.IsMaximal.isPrime` `primesOver_finite`
`prod_normalizedFactors_eq_self` 📖	mathematical	—	`Multiset.prod` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	—	`Ideal.uniqueFactorizationMonoid` `associated_iff_eq` `Unique.instSubsingleton` `UniqueFactorizationMonoid.prod_normalizedFactors`
`singleton_span_mem_normalizedFactors_of_mem_normalizedFactors` 📖	mathematical	`Multiset` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `PrincipalIdealRing.to_uniqueFactorizationMonoid`	`Ideal` `CommSemiring.toSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Ideal.span` `Set` `Set.instSingletonSet`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Ideal.span_singleton_eq_bot` `bot_eq_zero` `Submodule.instCanonicallyOrderedAdd` `UniqueFactorizationMonoid.normalizedFactors_zero` `Multiset.notMem_zero` `Ideal.prime_iff_isPrime` `Prime.ne_zero` `UniqueFactorizationMonoid.prime_of_normalized_factor` `Ideal.span_singleton_prime` `UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd` `Prime.irreducible` `Ideal.isCancelMulZero` `IsScalarTower.right` `Ideal.dvd_iff_le` `Ideal.span_singleton_le_span_singleton` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `associated_iff_eq` `Unique.instSubsingleton`
`span_singleton_dvd_span_singleton_iff_dvd` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing`	—	`IsScalarTower.right` `Ideal.mem_span_singleton` `Ideal.dvd_iff_le` `IsPrincipalIdealRing.isDedekindDomain` `dvd_refl` `dvd_trans`
`sup_eq_prod_inf_factors` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `Multiset.prod` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Multiset` `Multiset.instInter` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `Ideal.normalizationMonoid` `Ideal.uniqueFactorizationMonoid`	—	`Ideal.uniqueFactorizationMonoid` `UniqueFactorizationMonoid.normalizedFactors_prod_of_prime` `Unique.instSubsingleton` `UniqueFactorizationMonoid.prime_of_normalized_factor` `Multiset.mem_inter` `Multiset.prod_ne_zero_of_prime` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsDedekindDomain.toIsDomain` `Ideal.instNontrivial` `IsDomain.toNontrivial` `le_antisymm` `sup_le_iff` `IsScalarTower.right` `Ideal.dvd_iff_le` `UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors` `inf_le_left` `inf_le_right` `ne_bot_of_le_ne_bot` `le_sup_left` `Multiset.le_iff_count` `Multiset.count_inter` `le_min` `count_le_of_ideal_ge` `le_sup_right`

---

← Back to Index