Operations

📁 Source: Mathlib/RingTheory/FractionalIdeal/Operations.lean

Statistics

Metric	Count
Definitions adjoinIntegral, canonicalEquiv, instDivNonZeroDivisors, map, mapEquiv, spanFinset, spanSingleton, unitsMulEquivSubmodule	8
Theorems adjoinIntegral_coe, canonicalEquiv_canonicalEquiv, canonicalEquiv_coeIdeal, canonicalEquiv_def, canonicalEquiv_flip, canonicalEquiv_self, canonicalEquiv_spanSingleton, canonicalEquiv_symm, canonicalEquiv_trans_canonicalEquiv, coeFun_mapEquiv, coeIdeal_eq_one, coeIdeal_eq_zero, coeIdeal_fg, coeIdeal_inj, coeIdeal_injective, coeIdeal_ne_one, coeIdeal_ne_zero, coeIdeal_span_singleton, coe_div, coe_map, coe_spanSingleton, constant_factor_ne_zero, den_mul_self_eq_num', div_nonzero, div_of_ne_zero, div_one, div_spanSingleton, div_zero, eq_one_div_of_mul_eq_one_right, eq_spanSingleton_mul, eq_spanSingleton_of_principal, eq_zero_or_one, eq_zero_or_one_of_isField, exists_eq_spanSingleton_mul, exists_ne_zero_mem_isInteger, fg_of_isUnit, fg_unit, fractional_div_of_nonzero, ideal_factor_ne_zero, instNontrivialNonZeroDivisors, isFractional_adjoin_integral, isFractional_div_of_ne_zero, isFractional_of_fg, isFractional_span_iff, isFractional_span_singleton, isNoetherian, isNoetherian_coeIdeal, isNoetherian_iff, isNoetherian_spanSingleton_inv_to_map_mul, isNoetherian_zero, isPrincipal, isPrincipal_iff, isPrincipal_of_isPrincipal_num, le_div_iff_mul_le, le_div_iff_of_ne_zero, le_div_iff_of_nonzero, le_self_mul_one_div, le_spanSingleton_mul_iff, mapEquiv_apply, mapEquiv_refl, mapEquiv_symm, map_add, map_coeIdeal, map_comp, map_div, map_eq_zero_iff, map_id, map_injective, map_map_symm, map_mem_map, map_mul, map_ne_zero, map_one, map_one_div, map_symm_map, map_zero, mem_adjoinIntegral_self, mem_canonicalEquiv_apply, mem_div_iff_of_ne_zero, mem_div_iff_of_nonzero, mem_map, mem_singleton_mul, mem_spanSingleton, mem_spanSingleton_self, mem_span_mul_finite_of_mem_mul, mk'_mul_coeIdeal_eq_coeIdeal, mul_div_self_cancel_iff, mul_one_div_le_one, ne_zero_of_mul_eq_one, num_eq_zero_iff, num_le, one_div_spanSingleton, spanFinset_coe, spanFinset_eq_zero, spanFinset_ne_zero, spanSingleton_def, spanSingleton_eq_spanSingleton, spanSingleton_eq_zero_iff, spanSingleton_le_iff_mem, spanSingleton_mul_coeIdeal_eq_coeIdeal, spanSingleton_mul_le_iff, spanSingleton_mul_spanSingleton, spanSingleton_ne_zero_iff, spanSingleton_one, spanSingleton_pow, spanSingleton_zero, fg_of_isUnit, div_of_nonzero, map, submodule_isFractional	110
Total	118

FractionalIdeal

Definitions

Name	Category	Theorems
adjoinIntegral 📖	CompOp	2 math math: mem_adjoinIntegral_self, adjoinIntegral_coe
canonicalEquiv 📖	CompOp	14 math math: canonicalEquiv_trans_canonicalEquiv, canonicalEquiv_symm, canonicalEquiv_mk0, canonicalEquiv_spanSingleton, canonicalEquiv_coeIdeal, canonicalEquiv_canonicalEquiv, canonicalEquiv_flip, canonicalEquiv_def, map_canonicalEquiv_mk0, mem_canonicalEquiv_apply, canonicalEquiv_self, ClassGroup.mk_canonicalEquiv, ClassGroup.mk_def, ClassGroup.equiv_mk
instDivNonZeroDivisors 📖	CompOp	24 math math: map_one_div, div_one, le_div_iff_mul_le, le_div_iff_of_ne_zero, le_div_iff_of_nonzero, div_of_ne_zero, inv_eq, mem_div_iff_of_nonzero, one_div_spanSingleton, div_nonzero, eq_one_div_of_mul_eq_one_right, div_eq_mul_inv, coe_ideal_span_singleton_div_self, spanSingleton_div_spanSingleton, dual_div_dual, mul_one_div_le_one, map_div, div_spanSingleton, le_self_mul_one_div, div_zero, spanSingleton_div_self, coe_div, mem_div_iff_of_ne_zero, mul_div_self_cancel_iff
map 📖	CompOp	19 math math: mapEquiv_apply, map_one_div, mem_map, map_coeIdeal, map_comp, map_id, map_eq_zero_iff, coeFun_mapEquiv, map_div, map_inv, map_mul, coe_map, map_one, map_map_symm, map_add, map_symm_map, map_injective, map_mem_map, map_zero
mapEquiv 📖	CompOp	5 math math: mapEquiv_apply, mapEquiv_symm, coeFun_mapEquiv, canonicalEquiv_def, mapEquiv_refl
spanFinset 📖	CompOp	2 math math: spanFinset_eq_zero, spanFinset_coe
spanSingleton 📖	CompOp	42 math math: le_spanSingleton_mul_iff, spanSingleton_inv_mul, spanSingleton_mul_inv, coeIdeal_span_singleton, mem_principal_ideals_iff, mk'_mul_coeIdeal_eq_coeIdeal, spanSingleton_mul_spanSingleton, spanSingleton_le_iff_mem, one_div_spanSingleton, coe_toPrincipalIdeal, count_ne_zero, spanSingleton_pow, spanSingleton_mul_le_iff, mul_generator_self_inv, isNoetherian_spanSingleton_inv_to_map_mul, canonicalEquiv_spanSingleton, eq_spanSingleton_mul, isPrincipal_iff, spanSingleton_div_spanSingleton, mem_spanSingleton, absNorm_span_singleton, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, spanSingleton_zero, toPrincipalIdeal_eq_iff, eq_spanSingleton_of_principal, spanSingleton_mul_coeIdeal_eq_coeIdeal, div_spanSingleton, mem_singleton_mul, mem_spanSingleton_self, spanSingleton_eq_zero_iff, divMod_spec, IsDedekindDomain.exists_add_spanSingleton_mul_eq, spanSingleton_eq_spanSingleton, exists_eq_spanSingleton_mul, coe_spanSingleton, toPrincipalIdeal_def, spanSingleton_one, spanSingleton_div_self, spanSingleton_def, den_mul_self_eq_num', finprod_heightOneSpectrum_factorization_principal_fraction, spanSingleton_inv
unitsMulEquivSubmodule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoinIntegral_coe 📖	mathematical	IsIntegral CommRing.toRing	coeToSubmodule adjoinIntegral DFunLike.coe OrderEmbedding Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Algebra.adjoin Set Set.instSingletonSet	—	—
canonicalEquiv_canonicalEquiv 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv	—	ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomCompTriple.comp_eq RingHomCompTriple.ids IsLocalization.map_map IsLocalization.map.congr_simp
canonicalEquiv_coeIdeal 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv coeIdeal	—	ext IsLocalization.map_eq
canonicalEquiv_def 📖	mathematical	—	canonicalEquiv mapEquiv	—	—
canonicalEquiv_flip 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv	—	canonicalEquiv_symm RingEquiv.symm_apply_apply
canonicalEquiv_self 📖	mathematical	—	canonicalEquiv RingEquiv.refl FractionalIdeal instMul instAdd	—	canonicalEquiv_trans_canonicalEquiv canonicalEquiv_symm RingEquiv.symm_trans_self
canonicalEquiv_spanSingleton 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv spanSingleton RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike IsLocalization.map RingHom.id	—	SetLike.ext_iff mem_spanSingleton mem_canonicalEquiv_apply IsLocalization.map_smul RingHom.id_apply
canonicalEquiv_symm 📖	mathematical	—	RingEquiv.symm FractionalIdeal instMul instAdd canonicalEquiv	—	RingEquiv.ext SetLike.ext_iff mem_canonicalEquiv_apply canonicalEquiv_def mapEquiv_symm AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass mapEquiv_apply mem_map
canonicalEquiv_trans_canonicalEquiv 📖	mathematical	—	RingEquiv.trans FractionalIdeal instMul instAdd canonicalEquiv	—	RingEquiv.ext canonicalEquiv_canonicalEquiv
coeFun_mapEquiv 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv map AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	—
coeIdeal_eq_one 📖	mathematical	—	coeIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instOne Ideal Submodule.one Semiring.toModule	—	Ideal.one_eq_top
coeIdeal_eq_zero 📖	mathematical	—	coeIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instZero Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	coeIdeal_eq_zero' le_rfl
coeIdeal_fg 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Submodule.FG NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule coeIdeal Ideal.FG	—	IsLocalization.coeSubmodule_fg
coeIdeal_inj 📖	mathematical	—	coeIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing	—	coeIdeal_inj' le_rfl
coeIdeal_injective 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero Field.toCommRing coeIdeal	—	coeIdeal_injective' le_rfl
coeIdeal_ne_one 📖	—	—	—	—	not_iff_not coeIdeal_eq_one
coeIdeal_ne_zero 📖	—	—	—	—	coeIdeal_ne_zero' le_rfl
coeIdeal_span_singleton 📖	mathematical	—	coeIdeal Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet spanSingleton DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	ext mem_coeIdeal Submodule.mem_span_singleton smul_eq_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Algebra.smul_def mem_spanSingleton
coe_div 📖	mathematical	—	coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instDivNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.instDiv Semifield.toCommSemiring Field.toSemifield	—	isFractional_div_of_ne_zero
coe_map 📖	mathematical	—	coeToSubmodule map Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids AlgHom.toLinearMap	—	—
coe_spanSingleton 📖	mathematical	—	coeToSubmodule spanSingleton Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Set Set.instSingletonSet	—	isFractional_span_singleton spanSingleton_def
constant_factor_ne_zero 📖	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap coeIdeal	—	—	MulZeroClass.zero_mul spanSingleton_zero inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.span_singleton_eq_bot Ideal.zero_eq_bot
den_mul_self_eq_num' 📖	mathematical	—	FractionalIdeal instMul spanSingleton DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike den coeIdeal num	—	coeToSubmodule_injective IsScalarTower.right coe_mul smul_eq_mul coe_spanSingleton IsScalarTower.to_smulCommClass' Submodule.span_singleton_mul smulCommClass_self RingHomSurjective.ids Submodule.ext Submodule.mem_smul_pointwise_iff_exists Submonoid.smulCommClass_left Algebra.smul_def den_mul_self_eq_num
div_nonzero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule IsFractional Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule isFractional_div_of_ne_zero	—	div_of_ne_zero
div_of_ne_zero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule IsFractional Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule isFractional_div_of_ne_zero	—	isFractional_div_of_ne_zero
div_one 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors instOne	—	isFractional_div_of_ne_zero one_ne_zero' NeZero.one instNontrivialNonZeroDivisors div_of_ne_zero ext mul_one Submodule.mem_div_iff_forall_mul_mem coe_mem_one RingHom.map_one mul_comm Algebra.linearMap_apply Algebra.smul_def Submodule.smul_mem
div_spanSingleton 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors spanSingleton instMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	one_div_spanSingleton spanSingleton.congr_simp spanSingleton_zero div_zero MulZeroClass.zero_mul spanSingleton_eq_zero_iff le_antisymm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf mem_coe IsScalarTower.right coe_mul Submodule.mul_mem_mul mem_spanSingleton_self Submodule.mem_div_iff_forall_mul_mem coe_div le_div_iff_mul_le mul_assoc mul_left_comm spanSingleton_mul_spanSingleton inv_mul_cancel₀ spanSingleton_one le_refl
div_zero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors instZero	—	isFractional_div_of_ne_zero
eq_one_div_of_mul_eq_one_right 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instOne	instDivNonZeroDivisors	—	ne_zero_of_mul_eq_one le_antisymm mul_le mul_comm mem_div_iff_of_ne_zero mul_le_mul_right instMulLeftMono le_div_iff_of_ne_zero mul_mem_mul instIsDedekindFiniteMonoid Units.ext
eq_spanSingleton_mul 📖	mathematical	—	FractionalIdeal instMul spanSingleton SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
eq_spanSingleton_of_principal 📖	mathematical	—	spanSingleton Submodule.IsPrincipal.generator CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule	—	isFractional_span_singleton spanSingleton_def Submodule.IsPrincipal.span_singleton_generator
eq_zero_or_one 📖	mathematical	—	FractionalIdeal Field.toCommRing nonZeroDivisors Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instZero instOne	—	SetLike.ext_iff IsLocalization.exists_mk'_eq map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsFractionRing.mk'_eq_div exists_ne_zero_mem_isInteger IsLocalRing.toNontrivial Field.instIsLocalRing div_mul_cancel₀ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Algebra.smul_def Submodule.smul_mem
eq_zero_or_one_of_isField 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero Field.toCommRing instZero instOne	—	eq_zero_or_one
exists_eq_spanSingleton_mul 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap coeIdeal	—	isFractional mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial IsFractionRing.to_map_eq_zero_iff ext mem_coeIdeal mem_singleton_mul Algebra.smul_def mul_assoc inv_mul_cancel₀ one_mul Algebra.linearMap_apply
exists_ne_zero_mem_isInteger 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	SetLike.exists_of_lt instIsConcreteLE bot_lt_iff_ne_bot IsLocalization.exists_integer_multiple IsFractionRing.to_map_eq_zero_iff Algebra.smul_def mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors Submodule.smul_mem
fg_of_isUnit 📖	mathematical	IsUnit FractionalIdeal MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	Submodule.FG CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule	—	fg_unit
fg_unit 📖	mathematical	—	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule Units.val FractionalIdeal MonoidWithZero.toMonoid Semiring.toMonoidWithZero commSemiring	—	Submodule.fg_unit
fractional_div_of_nonzero 📖	mathematical	—	IsFractional nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule	—	isFractional_div_of_ne_zero
ideal_factor_ne_zero 📖	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap coeIdeal	—	—	MulZeroClass.mul_zero coeIdeal_bot Ideal.zero_eq_bot
instNontrivialNonZeroDivisors 📖	mathematical	—	Nontrivial FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing	—	RingHom.map_one coe_mem_one one_ne_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing mem_zero_iff
isFractional_adjoin_integral 📖	mathematical	IsIntegral CommRing.toRing	IsFractional DFunLike.coe OrderEmbedding Subalgebra CommRing.toCommSemiring Ring.toSemiring Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Algebra.adjoin Set Set.instSingletonSet	—	isFractional_of_fg IsIntegral.fg_adjoin_singleton
isFractional_div_of_ne_zero 📖	mathematical	—	IsFractional nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule	—	IsFractional.div_of_nonzero isFractional coeToSubmodule_injective coe_zero
isFractional_of_fg 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	IsFractional	—	IsLocalization.exist_integer_multiples_of_finset isFractional_span_iff
isFractional_span_iff 📖	mathematical	—	IsFractional Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike IsLocalization.IsInteger Algebra.toSMul	—	Submodule.subset_span Submodule.span_induction smul_zero IsLocalization.isInteger_zero smul_add IsLocalization.isInteger_add SMulCommClass.smul_comm smulCommClass_self IsLocalization.isInteger_smul
isFractional_span_singleton 📖	mathematical	—	IsFractional Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Set Set.instSingletonSet	—	IsLocalization.exists_integer_multiple isFractional_span_iff Set.mem_singleton_iff
isNoetherian 📖	mathematical	—	IsNoetherian Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule SetLike.instMembership Submodule.setLike coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Submodule.addCommMonoid instModuleSubtypeMemSubmoduleCoeToSubmodule	—	exists_eq_spanSingleton_mul isNoetherian_spanSingleton_inv_to_map_mul isNoetherian_coeIdeal
isNoetherian_coeIdeal 📖	mathematical	—	IsNoetherian Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule SetLike.instMembership Submodule.setLike coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero coeIdeal Submodule.addCommMonoid instModuleSubtypeMemSubmoduleCoeToSubmodule	—	isNoetherian_iff le_one_iff_exists_coeIdeal le_trans coeIdeal_le_one Submodule.FG.map RingHomSurjective.ids IsNoetherian.noetherian
isNoetherian_iff 📖	mathematical	—	IsNoetherian Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule SetLike.instMembership Submodule.setLike coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Submodule.addCommMonoid instModuleSubtypeMemSubmoduleCoeToSubmodule Submodule.FG	—	isNoetherian_submodule isFractional_of_le
isNoetherian_spanSingleton_inv_to_map_mul 📖	mathematical	—	IsNoetherian Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule SetLike.instMembership Submodule.setLike coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero FractionalIdeal instMul spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Submodule.addCommMonoid instModuleSubtypeMemSubmoduleCoeToSubmodule	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass inv_zero spanSingleton_zero MulZeroClass.zero_mul isNoetherian_zero injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass IsFractionRing.injective spanSingleton_ne_zero_iff isNoetherian_iff le_div_iff_mul_le div_spanSingleton Finset.coe_mul Finset.coe_singleton IsScalarTower.right Submodule.span_mul_span coe_spanSingleton coe_mul mul_assoc spanSingleton_mul_spanSingleton mul_inv_cancel₀ spanSingleton_one mul_one
isNoetherian_zero 📖	mathematical	—	IsNoetherian Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule SetLike.instMembership Submodule.setLike coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero FractionalIdeal instZero Submodule.addCommMonoid instModuleSubtypeMemSubmoduleCoeToSubmodule	—	isNoetherian_submodule le_bot_iff coe_zero Submodule.fg_bot
isPrincipal 📖	mathematical	—	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero	—	exists_eq_spanSingleton_mul IsPrincipalIdealRing.principal Submodule.IsPrincipal.span_singleton_generator Ideal.submodule_span_eq coeIdeal_span_singleton spanSingleton_mul_spanSingleton isFractional_span_singleton spanSingleton_def
isPrincipal_iff 📖	mathematical	—	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule spanSingleton	—	eq_spanSingleton_of_principal coe_spanSingleton
isPrincipal_of_isPrincipal_num 📖	mathematical	—	Submodule.IsPrincipal FractionRing CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing OreLocalization.instCommRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.toModule OreLocalization.instAlgebra Algebra.id coeToSubmodule	—	Module.isPrincipal_submodule_iff LinearEquiv.isPrincipal_iff FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial Localization.isLocalization
le_div_iff_mul_le 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instDivNonZeroDivisors instMul	—	isFractional_div_of_ne_zero div_of_ne_zero coe_le_coe IsScalarTower.right coe_mul Submodule.le_div_iff_mul_le
le_div_iff_of_ne_zero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instDivNonZeroDivisors SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mem_div_iff_of_ne_zero
le_div_iff_of_nonzero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instDivNonZeroDivisors SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_div_iff_of_ne_zero
le_self_mul_one_div 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instOne	instMul instDivNonZeroDivisors	—	div_zero MulZeroClass.mul_zero le_refl coe_le_coe IsScalarTower.right coe_mul coe_div coe_one Submodule.le_self_mul_one_div
le_spanSingleton_mul_iff 📖	mathematical	—	FractionalIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder instMul spanSingleton SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
mapEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv map AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	—
mapEquiv_refl 📖	mathematical	—	mapEquiv AlgEquiv.refl CommRing.toCommSemiring CommSemiring.toSemiring RingEquiv.refl FractionalIdeal instMul instAdd	—	RingEquiv.ext map_id
mapEquiv_symm 📖	mathematical	—	RingEquiv.symm FractionalIdeal instMul instAdd mapEquiv AlgEquiv.symm CommRing.toCommSemiring CommSemiring.toSemiring	—	—
map_add 📖	mathematical	—	map FractionalIdeal instAdd	—	coeToSubmodule_injective Submodule.map_sup RingHomSurjective.ids
map_coeIdeal 📖	mathematical	—	map coeIdeal	—	ext AlgHom.commutes
map_comp 📖	mathematical	—	map AlgHom.comp CommRing.toCommSemiring CommSemiring.toSemiring	—	coeToSubmodule_injective Submodule.map_comp RingHomCompTriple.ids RingHomSurjective.ids
map_div 📖	mathematical	—	map nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing AlgHomClass.toAlgHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass FractionalIdeal instDivNonZeroDivisors	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass div_zero map_zero isFractional_div_of_ne_zero RingHomSurjective.ids map_ne_zero IsDomain.toNontrivial div_of_ne_zero Submodule.map_div
map_eq_zero_iff 📖	mathematical	—	map nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instZero	—	not_imp_not map_ne_zero map_zero
map_id 📖	mathematical	—	map AlgHom.id CommRing.toCommSemiring CommSemiring.toSemiring	—	coeToSubmodule_injective Submodule.map_id
map_injective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	FractionalIdeal map	—	ext map_mem_map
map_map_symm 📖	mathematical	—	map AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.symm	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_comp AlgEquiv.symm_comp map_id
map_mem_map 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	FractionalIdeal SetLike.instMembership instSetLike map	—	mem_map
map_mul 📖	mathematical	—	map FractionalIdeal instMul	—	IsScalarTower.right IsFractional.mul isFractional mul_def coeToSubmodule_injective Submodule.map_mul
map_ne_zero 📖	—	—	—	—	exists_ne_zero_mem_isInteger Mathlib.Tactic.Contrapose.contrapose₄ IsFractionRing.to_map_eq_zero_iff eq_zero_iff mem_map AlgHom.commutes
map_one 📖	mathematical	—	map FractionalIdeal instOne	—	map_coeIdeal
map_one_div 📖	mathematical	—	map nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing AlgHomClass.toAlgHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass FractionalIdeal instDivNonZeroDivisors instOne	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_div map_one
map_symm_map 📖	mathematical	—	map AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.symm	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_comp AlgEquiv.comp_symm map_id
map_zero 📖	mathematical	—	map FractionalIdeal instZero	—	map_coeIdeal
mem_adjoinIntegral_self 📖	mathematical	IsIntegral CommRing.toRing	FractionalIdeal SetLike.instMembership instSetLike adjoinIntegral	—	Algebra.subset_adjoin Set.mem_singleton
mem_canonicalEquiv_apply 📖	mathematical	—	FractionalIdeal SetLike.instMembership instSetLike DFunLike.coe RingEquiv instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike IsLocalization.map RingHom.id	—	canonicalEquiv_def AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass mapEquiv_apply mem_map
mem_div_iff_of_ne_zero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing SetLike.instMembership instSetLike instDivNonZeroDivisors Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	isFractional_div_of_ne_zero div_of_ne_zero Submodule.mem_div_iff_forall_mul_mem
mem_div_iff_of_nonzero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing SetLike.instMembership instSetLike instDivNonZeroDivisors Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mem_div_iff_of_ne_zero
mem_map 📖	mathematical	—	FractionalIdeal SetLike.instMembership instSetLike map DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	Submodule.mem_map RingHomSurjective.ids
mem_singleton_mul 📖	mathematical	—	FractionalIdeal SetLike.instMembership instSetLike instMul spanSingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mul_induction_on mem_spanSingleton Submodule.smul_mem Algebra.mul_smul_comm Algebra.smul_mul_assoc Submodule.add_mem mul_add Distrib.leftDistribClass mul_mem_mul one_smul
mem_spanSingleton 📖	mathematical	—	FractionalIdeal SetLike.instMembership instSetLike spanSingleton Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	isFractional_span_singleton spanSingleton_def Submodule.mem_span_singleton
mem_spanSingleton_self 📖	mathematical	—	FractionalIdeal SetLike.instMembership instSetLike spanSingleton	—	mem_spanSingleton one_smul
mem_span_mul_finite_of_mem_mul 📖	mathematical	FractionalIdeal SetLike.instMembership instSetLike instMul	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.setLike Submodule.span Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Submodule.mem_span_mul_finite_of_mem_mul IsScalarTower.right coe_mul mem_coe
mk'_mul_coeIdeal_eq_coeIdeal 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	FractionalIdeal Field.toCommRing instMul spanSingleton IsLocalization.mk' Semifield.toCommSemiring Field.toSemifield NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring coeIdeal Ideal Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Ideal.span Set Set.instSingletonSet	—	spanSingleton_mul_spanSingleton mul_comm IsLocalization.mk'_eq_mul_mk'_one IsLocalization.mk'_self spanSingleton_one instIsDedekindFiniteMonoid IsScalarTower.right coeIdeal_mul coeIdeal_span_singleton mul_assoc one_mul
mul_div_self_cancel_iff 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instDivNonZeroDivisors instOne	—	eq_one_div_of_mul_eq_one_right
mul_one_div_le_one 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instMul instDivNonZeroDivisors instOne	—	div_zero MulZeroClass.mul_zero zero_le coe_le_coe IsScalarTower.right coe_mul coe_div coe_one Submodule.mul_one_div_le_one
ne_zero_of_mul_eq_one 📖	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instOne	—	—	zero_ne_one' NeZero.one instNontrivialNonZeroDivisors MulZeroClass.zero_mul
num_eq_zero_iff 📖	mathematical	—	num nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Ideal Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule FractionalIdeal instZero	—	zero_of_num_eq_bot FaithfulSMul.to_isTorsionFree Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsLocalRing.toNontrivial Field.instIsLocalRing IsFractionRing.instFaithfulSMul IsDomain.toNontrivial instIsDomain zero_notMem_nonZeroDivisors num_zero_eq IsFractionRing.injective
num_le 📖	mathematical	—	FractionalIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder coeIdeal num	—	den_mul_self_eq_num' spanSingleton_mul_le_iff Algebra.smul_def Submodule.smul_mem
one_div_spanSingleton 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors instOne spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	spanSingleton.congr_simp spanSingleton_zero div_zero inv_zero eq_one_div_of_mul_eq_one_right spanSingleton_mul_spanSingleton mul_inv_cancel₀ spanSingleton_one
spanFinset_coe 📖	mathematical	—	coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing spanFinset Submodule.span NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Set.image SetLike.coe Finset Finset.instSetLike	—	—
spanFinset_eq_zero 📖	mathematical	—	spanFinset FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coe_zero
spanFinset_ne_zero 📖	mathematical	—	Finset Finset.instMembership	—	—
spanSingleton_def 📖	mathematical	—	spanSingleton Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule IsFractional Submodule.span Set Set.instSingletonSet isFractional_span_singleton	—	isFractional_span_singleton
spanSingleton_eq_spanSingleton 📖	mathematical	—	spanSingleton Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instSMul Algebra.toSMul	—	Submodule.span_singleton_eq_span_singleton isFractional_span_singleton spanSingleton_def
spanSingleton_eq_zero_iff 📖	mathematical	—	spanSingleton FractionalIdeal instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.span_eq_bot coe_spanSingleton coe_zero Set.mem_singleton spanSingleton.congr_simp spanSingleton_zero
spanSingleton_le_iff_mem 📖	mathematical	—	FractionalIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder spanSingleton SetLike.instMembership instSetLike	—	coe_le_coe coe_spanSingleton Submodule.span_singleton_le_iff_mem mem_coe
spanSingleton_mul_coeIdeal_eq_coeIdeal 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul spanSingleton coeIdeal Ideal Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Ideal.span Set Set.instSingletonSet Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike IsLocalization.sec Semifield.toCommSemiring Field.toSemifield	—	IsScalarTower.right Subtype.prop mk'_mul_coeIdeal_eq_coeIdeal IsLocalization.mk'_sec
spanSingleton_mul_le_iff 📖	mathematical	—	FractionalIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder instMul spanSingleton SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	one_smul Algebra.smul_mul_assoc Submodule.smul_mem
spanSingleton_mul_spanSingleton 📖	mathematical	—	FractionalIdeal instMul spanSingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coeToSubmodule_injective IsScalarTower.right coe_mul coe_spanSingleton Submodule.span_mul_span Set.singleton_mul_singleton
spanSingleton_ne_zero_iff 📖	—	—	—	—	spanSingleton_eq_zero_iff
spanSingleton_one 📖	mathematical	—	spanSingleton AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing FractionalIdeal instOne	—	ext mem_spanSingleton Algebra.smul_def mul_one mem_one_iff
spanSingleton_pow 📖	mathematical	—	FractionalIdeal instPowNat spanSingleton Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	pow_zero spanSingleton_one pow_succ spanSingleton_mul_spanSingleton
spanSingleton_zero 📖	mathematical	—	spanSingleton MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing FractionalIdeal instZero	—	ext smul_zero Zero.instNonempty

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_isUnit 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap IsUnit FractionalIdeal MonoidWithZero.toMonoid Semiring.toMonoidWithZero FractionalIdeal.commSemiring FractionalIdeal.coeIdeal	FG	—	FractionalIdeal.coeIdeal_fg FractionalIdeal.fg_of_isUnit

IsFractional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_of_nonzero 📖	mathematical	IsFractional nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.instDiv Semifield.toCommSemiring	—	SetLike.exists_of_lt instIsConcreteLE bot_lt_iff_ne_bot Submonoid.mul_mem mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial Algebra.smul_def map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_eq_zero instIsDomain injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass IsFractionRing.injective mul_comm SemigroupAction.mul_smul Submodule.smul_mem
map 📖	mathematical	IsFractional	Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule RingHom.id RingHomSurjective.ids AlgHom.toLinearMap	—	RingHomSurjective.ids Submodule.mem_map AlgHom.commutes map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AlgHom.toLinearMap_apply

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
submodule_isFractional 📖	mathematical	—	IsFractional val Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring	—	FractionalIdeal.isFractional_of_fg Submodule.fg_unit

---

← Back to Index