Basic

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

Statistics

Metric	Count
Definitions semifield, normalizationMonoid, IsDedekindDomainInv, commGroupWithZero	4
Theorems adjoinIntegral_eq_one_of_isUnit, coe_ideal_mul_inv, instMulPosReflectLENonZeroDivisors, instMulPosStrictMonoNonZeroDivisors, instPosMulReflectLEIdealOfIsDedekindDomain, instPosMulReflectLENonZeroDivisors, instPosMulStrictMonoNonZeroDivisors, mul_inv_cancel_of_le_one, mul_left_strictMono, mul_right_strictMono, not_inv_le_one_of_ne_bot, dvdNotUnit_iff_lt, dvd_iff_le, isCancelMulZero, isDomain, liesOver_iff_dvd_map, uniqueFactorizationMonoid, dimensionLEOne, integrallyClosed, isDedekindDomain, isNoetherianRing, exists_multiset_prod_cons_le_and_prod_not_le, instMulPosStrictMonoIdeal, instPosMulStrictMonoIdeal, instWfDvdMonoidIdeal, isDedekindDomainInv_iff, isDedekindDomain_iff_isDedekindDomainInv, one_mem_inv_coe_ideal	28
Total	32

FractionalIdeal

Definitions

Name	Category	Theorems
semifield 📖	CompOp	39 math math: finprod_heightOneSpectrum_factorization_principal, Ideal.hasFiniteMulSupport_coe, ClassGroup.mk0_integralRep, NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, NumberField.mixedEmbedding.mem_idealLattice, count_finsuppProd, count_finprod_coprime, finprod_heightOneSpectrum_factorization, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, count_finprod, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.span_idealLatticeBasis, canonicalEquiv_mk0, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, ClassGroup.mk_mk0, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, Ideal.finite_mulSupport_coe, NumberField.fractionalIdeal_rank, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, count_zpow_self, count_neg_zpow, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', NumberField.mem_span_basisOfFractionalIdeal, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, count_zpow, map_canonicalEquiv_mk0, Ideal.finprod_heightOneSpectrum_factorization_coe, NumberField.basisOfFractionalIdeal_apply, ClassGroup.equiv_mk0, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, Ideal.hasFiniteMulSupport_inv, finprod_heightOneSpectrum_factorization_principal_fraction, Ideal.finite_mulSupport_inv, coe_mk0, finprod_heightOneSpectrum_factorization'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoinIntegral_eq_one_of_isUnit 📖	mathematical	IsIntegral DivisionRing.toRing Field.toDivisionRing IsUnit FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid commSemiring adjoinIntegral	adjoinIntegral nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal instOne	—	coeToSubmodule_injective IsScalarTower.right coe_mul Subalgebra.isIdempotentElem_toSubmodule mul_assoc mul_inv_cancel_iff_isUnit mul_one
coe_ideal_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul coeIdeal instInvNonZeroDivisors IsDedekindDomain.toIsDomain instOne	—	mul_inv_cancel_of_le_one IsDedekindDomain.toIsDomain inv_zero' zero_le mem_integralClosure_iff_mem_fg mem_inv_iff coeIdeal_ne_zero mul_assoc mul_comm mul_mem_mul isNoetherian_submodule isNoetherian IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing AlgHom.mem_range Polynomial.aeval_eq_sum_range Submodule.sum_mem Submodule.smul_mem pow_zero one_mem_inv_coe_ideal pow_succ' Polynomial.aeval_X mem_one_iff Set.mem_range Algebra.mem_bot IsIntegrallyClosed.integralClosure_eq_bot IsDedekindRing.toIsIntegralClosure
instMulPosReflectLENonZeroDivisors 📖	mathematical	—	MulPosReflectLE FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instZero PartialOrder.toPreorder instPartialOrder	—	IsDedekindDomain.toIsDomain mul_inv_cancel_right₀ LT.lt.ne' mul_left_mono instMulRightMono
instMulPosStrictMonoNonZeroDivisors 📖	mathematical	—	MulPosStrictMono FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instZero PartialOrder.toPreorder instPartialOrder	—	MulPosMono.toMulPosStrictMono IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain IsOrderedRing.toMulPosMono instIsOrderedRing
instPosMulReflectLEIdealOfIsDedekindDomain 📖	mathematical	—	PosMulReflectLE Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PartialOrder.toPreorder Submodule.instPartialOrder	—	IsScalarTower.right coeIdeal_le_coeIdeal Localization.isLocalization mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono IsDedekindDomain.toIsDomain instIsOrderedRing instPosMulReflectLENonZeroDivisors instCanonicallyOrderedAdd LT.lt.ne' coeIdeal_mul
instPosMulReflectLENonZeroDivisors 📖	mathematical	—	PosMulReflectLE FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instZero PartialOrder.toPreorder instPartialOrder	—	IsDedekindDomain.toIsDomain inv_mul_cancel_left₀ LT.lt.ne' mul_right_mono instMulLeftMono
instPosMulStrictMonoNonZeroDivisors 📖	mathematical	—	PosMulStrictMono FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instZero PartialOrder.toPreorder instPartialOrder	—	PosMulMono.toPosMulStrictMono IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain IsOrderedRing.toPosMulMono instIsOrderedRing
mul_inv_cancel_of_le_one 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder instPartialOrder instInvNonZeroDivisors IsDedekindDomain.toIsDomain instMul coeIdeal instOne	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul coeIdeal instInvNonZeroDivisors IsDedekindDomain.toIsDomain instOne	—	IsDedekindDomain.toIsDomain le_one_iff_exists_coeIdeal mul_one_div_le_one eq_bot_iff coeIdeal_le_coeIdeal coe_ideal_le_self_mul_inv coeIdeal_top not_inv_le_one_of_ne_bot
mul_left_strictMono 📖	mathematical	—	StrictMono FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain PartialOrder.toPreorder instPartialOrder instMul	—	mul_lt_mul_of_pos_right instMulPosStrictMonoNonZeroDivisors pos_iff_ne_zero instCanonicallyOrderedAdd
mul_right_strictMono 📖	mathematical	—	StrictMono FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain PartialOrder.toPreorder instPartialOrder instMul	—	mul_lt_mul_of_pos_left instPosMulStrictMonoNonZeroDivisors pos_iff_ne_zero instCanonicallyOrderedAdd
not_inv_le_one_of_ne_bot 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder instPartialOrder instInvNonZeroDivisors IsDedekindDomain.toIsDomain coeIdeal instOne	—	IsSimpleOrder.eq_bot_or_eq_top Ideal.isSimpleOrder IsDedekindDomain.toIsDomain Ideal.bot_lt_of_maximal IsDomain.toNontrivial Submodule.nonzero_mem_of_bot_lt Subtype.coe_injective Ideal.span_singleton_eq_bot Ideal.span_singleton_le_iff_mem exists_multiset_prod_cons_le_and_prod_not_le SetLike.not_le_iff_exists instIsConcreteLE injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass IsFractionRing.injective Set.not_subset mem_inv_iff coeIdeal_ne_zero LT.lt.ne' mem_coeIdeal mul_comm mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Multiset.prod_cons Submodule.smul_mem_smul IsScalarTower.right Ideal.mem_span_singleton' mul_inv_cancel₀ mul_one coe_mem_one mem_one_iff eq_div_iff_mul_eq div_eq_mul_inv Ideal.exists_le_maximal le_trans inv_anti_mono Ideal.IsMaximal.ne_top

Ideal

Definitions

Name	Category	Theorems
normalizationMonoid 📖	CompOp	24 math math: normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, prod_normalizedFactors_eq_self, count_normalizedFactors_eq, IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, normalizedFactorsEquivOfQuotEquiv_symm, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, count_span_normalizedFactors_eq_of_normUnit, irreducible_pow_sup, mem_normalizedFactors_iff, count_le_of_ideal_ge, mem_primesOver_iff_mem_normalizedFactors, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, count_span_normalizedFactors_eq, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, eq_prime_pow_mul_coprime, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, count_associates_factors_eq, sup_eq_prod_inf_factors, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvdNotUnit_iff_lt 📖	mathematical	—	DvdNotUnit Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring instIdemCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	lt_of_le_of_ne IsScalarTower.right dvd_iff_le mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero isCancelMulZero mul_one isUnit_one dvdNotUnit_of_dvd_of_not_dvd le_of_lt not_le_of_gt
dvd_iff_le 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring 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	—	IsScalarTower.right le_of_dvd eq_bot_iff dvd_refl IsDedekindDomain.toIsDomain FractionalIdeal.coeIdeal_ne_zero Localization.isLocalization inv_mul_cancel₀ mul_le_mul_right FractionalIdeal.instMulLeftMono FractionalIdeal.le_one_iff_exists_coeIdeal FractionalIdeal.coeIdeal_injective FractionalIdeal.coeIdeal_mul mul_assoc mul_inv_cancel₀ one_mul
isCancelMulZero 📖	mathematical	—	IsCancelMulZero Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Function.Injective.isCancelMulZero IsScalarTower.right FractionalIdeal.coeIdeal_injective IsDedekindDomain.toIsDomain Localization.isLocalization map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsDomain.toIsCancelMulZero instIsDomain
isDomain 📖	mathematical	—	IsDomain Ideal CommSemiring.toSemiring CommRing.toCommSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	—	isCancelMulZero instNontrivial IsDomain.toNontrivial IsDedekindDomain.toIsDomain
liesOver_iff_dvd_map 📖	mathematical	—	LiesOver CommRing.toCommSemiring CommSemiring.toSemiring Ideal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Submodule.instNonUnitalSemiring Semiring.toModule IsScalarTower.right Algebra.id map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.right liesOver_iff dvd_iff_le RingHom.instRingHomClass under_def map_le_iff_le_comap IsCoatom.le_iff_eq isMaximal_def comap_ne_top
uniqueFactorizationMonoid 📖	mathematical	—	UniqueFactorizationMonoid Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring instIdemCommSemiring	—	isCancelMulZero instWfDvdMonoidIdeal Irreducible.ne_zero Irreducible.not_isUnit isUnit_iff dvdNotUnit_iff_lt Irreducible.isUnit_or_isUnit IsScalarTower.right dvd_iff_le SetLike.le_def instIsConcreteLE Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq mul_mem_mul IsPrime.mem_or_mem IsMaximal.isPrime Prime.irreducible

IsDedekindDomainInv

Definitions

Name	Category	Theorems
commGroupWithZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dimensionLEOne 📖	mathematical	IsDedekindDomainInv	Ring.DimensionLEOne	—	Localization.isLocalization Ideal.isMaximal_def Ideal.IsPrime.ne_top FractionalIdeal.coeIdeal_ne_zero LT.lt.ne_bot inv_mul_cancel₀ mul_le_mul_right FractionalIdeal.instMulLeftMono le_of_lt FractionalIdeal.mem_coeIdeal SetLike.exists_of_lt instIsConcreteLE FractionalIdeal.mul_mem_mul FractionalIdeal.mem_coeIdeal_of_mem one_mul mul_inv_cancel₀ mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Ideal.IsPrime.mem_or_mem IsFractionRing.injective eq_top_iff FractionalIdeal.coeIdeal_le_coeIdeal FractionalIdeal.coeIdeal_top mul_inv_cancel_left₀ mul_le_mul_left FractionalIdeal.instMulRightMono
integrallyClosed 📖	mathematical	IsDedekindDomainInv	IsIntegrallyClosed	—	Localization.isLocalization isIntegrallyClosed_iff Set.mem_range Algebra.mem_bot Subalgebra.mem_toSubmodule Algebra.toSubmodule_bot Submodule.one_eq_span FractionalIdeal.coe_spanSingleton FractionalIdeal.spanSingleton_one FractionalIdeal.adjoinIntegral_eq_one_of_isUnit Ne.isUnit one_ne_zero NeZero.one FractionRing.instNontrivial IsDomain.toNontrivial FractionalIdeal.eq_zero_iff Subalgebra.one_mem FractionalIdeal.mem_adjoinIntegral_self
isDedekindDomain 📖	mathematical	IsDedekindDomainInv	IsDedekindDomain	—	isNoetherianRing dimensionLEOne integrallyClosed
isNoetherianRing 📖	mathematical	IsDedekindDomainInv	IsNoetherianRing CommSemiring.toSemiring CommRing.toCommSemiring	—	Localization.isLocalization isNoetherianRing_iff Submodule.fg_bot FractionalIdeal.coeIdeal_ne_zero Ideal.fg_of_isUnit IsFractionRing.injective Ne.isUnit

(root)

Definitions

Name	Category	Theorems
IsDedekindDomainInv 📖	MathDef	2 math math: isDedekindDomain_iff_isDedekindDomainInv, isDedekindDomainInv_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_multiset_prod_cons_le_and_prod_not_le 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Multiset PrimeSpectrum CommRing.toCommSemiring Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Multiset.prod CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Multiset.cons Multiset.map PrimeSpectrum.asIdeal	—	PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain IsDedekindDomain.toIsDomain IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing WellFounded.has_min wellFounded_lt Multiset.instWellFoundedLT Ideal.IsPrime.multiset_prod_le Ideal.IsMaximal.isPrime LE.le.trans Multiset.mem_map Multiset.map_erase PrimeSpectrum.ext IsScalarTower.left Ideal.mul_eq_bot IsDomain.to_noZeroDivisors Multiset.prod_cons Multiset.cons_erase Ideal.IsMaximal.eq_of_le Ideal.IsPrime.isMaximal IsDedekindRing.toDimensionLEOne PrimeSpectrum.isPrime Ideal.IsMaximal.ne_top Multiset.erase_lt
instMulPosStrictMonoIdeal 📖	mathematical	—	MulPosStrictMono Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PartialOrder.toPreorder Submodule.instPartialOrder	—	MulPosMono.toMulPosStrictMono IsCancelMulZero.toIsRightCancelMulZero Ideal.isCancelMulZero IsOrderedRing.toMulPosMono Submodule.instIsOrderedRing
instPosMulStrictMonoIdeal 📖	mathematical	—	PosMulStrictMono Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PartialOrder.toPreorder Submodule.instPartialOrder	—	PosMulMono.toPosMulStrictMono IsCancelMulZero.toIsLeftCancelMulZero Ideal.isCancelMulZero IsOrderedRing.toPosMulMono Submodule.instIsOrderedRing
instWfDvdMonoidIdeal 📖	mathematical	—	WfDvdMonoid Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring	—	wellFoundedGT IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing Ideal.dvdNotUnit_iff_lt IsWellFounded.wf
isDedekindDomainInv_iff 📖	mathematical	—	IsDedekindDomainInv FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.instMul FractionalIdeal.instInvNonZeroDivisors FractionalIdeal.instOne	—	Equiv.forall_congr Equiv.apply_eq_iff_eq AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass FractionalIdeal.map_mul FractionalIdeal.map_inv FractionalIdeal.map_one Localization.isLocalization IsDomain.toNontrivial
isDedekindDomain_iff_isDedekindDomainInv 📖	mathematical	—	IsDedekindDomain IsDedekindDomainInv	—	mul_inv_cancel₀ Localization.isLocalization IsDedekindDomainInv.isDedekindDomain
one_mem_inv_coe_ideal 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership FractionalIdeal.instSetLike FractionalIdeal.instInvNonZeroDivisors FractionalIdeal.coeIdeal AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	FractionalIdeal.mem_inv_iff FractionalIdeal.coeIdeal_ne_zero one_mul FractionalIdeal.coeIdeal_le_one

---

← Back to Index