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, div_eq_mul_inv, instMulPosReflectLENonZeroDivisors, instMulPosStrictMonoNonZeroDivisors, instPosMulReflectLEIdealOfIsDedekindDomain, instPosMulReflectLENonZeroDivisors, instPosMulStrictMonoNonZeroDivisors, mul_inv_cancel, mul_inv_cancel_of_le_one, mul_left_le_iff, mul_left_strictMono, mul_right_le_iff, 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, inv_mul_eq_one, isDedekindDomain, isNoetherianRing, mul_inv_eq_one, exists_multiset_prod_cons_le_and_prod_not_le, instMulPosStrictMonoIdeal, instPosMulStrictMonoIdeal, instWfDvdMonoidIdeal, isDedekindDomainInv_iff, isDedekindDomain_iff_isDedekindDomainInv, one_mem_inv_coe_ideal	34
Total	38

FractionalIdeal

Definitions

Name	Category	Theorems
semifield 📖	CompOp	37 math math: finprod_heightOneSpectrum_factorization_principal, 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, 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	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
div_eq_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instDivNonZeroDivisors IsDedekindDomain.toIsDomain instMul instInvNonZeroDivisors	—	div_eq_mul_inv
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 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instInvNonZeroDivisors IsDedekindDomain.toIsDomain instOne	—	mul_inv_cancel₀
mul_inv_cancel_of_le_one 📖	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder instPartialOrder instInvNonZeroDivisors IsDedekindDomain.toIsDomain instMul coeIdeal 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_le_iff 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder instPartialOrder instMul	—	mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono instIsOrderedRing instPosMulReflectLENonZeroDivisors pos_iff_ne_zero instCanonicallyOrderedAdd
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_le_iff 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder instPartialOrder instMul	—	mul_le_mul_iff_left₀ IsOrderedRing.toMulPosMono instIsOrderedRing instMulPosReflectLENonZeroDivisors 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	21 math math: prod_normalizedFactors_eq_self, count_normalizedFactors_eq, IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, normalizedFactorsEquivOfQuotEquiv_symm, 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
inv_mul_eq_one 📖	mathematical	IsDedekindDomainInv	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.instMul FractionalIdeal.instInvNonZeroDivisors FractionalIdeal.instOne	—	inv_mul_cancel₀
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
mul_inv_eq_one 📖	mathematical	IsDedekindDomainInv	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.instMul FractionalIdeal.instInvNonZeroDivisors FractionalIdeal.instOne	—	mul_inv_cancel₀

(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.prod CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Multiset.cons Multiset.map PrimeSpectrum 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