Inverse

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

Statistics

Metric	Count
Definitions instInvNonZeroDivisors, instInvOneClassNonZeroDivisors	2
Theorems bot_lt_mul_inv, coe_ideal_le_self_mul_inv, coe_ideal_span_singleton_div_self, coe_ideal_span_singleton_inv_mul, coe_ideal_span_singleton_mul_inv, coe_inv_of_ne_zero, coe_inv_of_nonzero, den_mem_inv, inv_anti_mono, inv_eq, inv_nonzero, inv_of_ne_zero, inv_zero', invertible_iff_generator_nonzero, invertible_of_principal, isPrincipal_inv, le_self_mul_inv, map_inv, mem_inv_iff, mul_generator_self_inv, mul_inv_cancel_iff, mul_inv_cancel_iff_isUnit, num_le_mul_inv, right_inverse_eq, spanSingleton_div_self, spanSingleton_div_spanSingleton, spanSingleton_inv, spanSingleton_inv_mul, spanSingleton_mul_inv	29
Total	31

FractionalIdeal

Definitions

Name	Category	Theorems
instInvNonZeroDivisors 📖	CompOp	45 math math: spanSingleton_inv_mul, spanSingleton_mul_inv, inv_anti_mono, invertible_of_principal, inv_le_inv_iff, right_inverse_eq, inv_nonzero, le_self_mul_inv, inv_eq, mul_inv_cancel, differentialIdeal_le_iff, coeIdeal_differentIdeal, inv_le_dual, div_eq_mul_inv, le_inv_comm, IsDedekindDomainInv.mul_inv_eq_one, num_le_mul_inv, coe_inv_of_ne_zero, differentialIdeal_le_fractionalIdeal_iff, dual_eq_mul_inv, one_mem_inv_coe_ideal, isPrincipal_inv, coe_ideal_mul_inv, map_inv, mul_inv_cancel_iff, coe_ideal_span_singleton_inv_mul, coe_inv_of_nonzero, IsDedekindDomainInv.inv_mul_eq_one, dual_inv, bot_lt_mul_inv, not_inv_le_one_of_ne_bot, mul_inv_cancel_iff_isUnit, inv_zero', count_inv, invertible_iff_generator_nonzero, dual_inv_le, coe_ideal_span_singleton_mul_inv, inv_le_comm, den_mem_inv, isDedekindDomainInv_iff, coe_ideal_le_self_mul_inv, mem_inv_iff, spanSingleton_inv, inv_of_ne_zero, exists_notMem_one_of_ne_bot
instInvOneClassNonZeroDivisors 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLT PartialOrder.toPreorder instPartialOrder Bot.bot OrderBot.toBot Preorder.toLE orderBot instMul instInvNonZeroDivisors	—	lt_of_lt_of_le Ne.bot_lt coeIdeal_ne_zero num_eq_zero_iff num_le_mul_inv
coe_ideal_le_self_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder coeIdeal instMul instInvNonZeroDivisors	—	le_self_mul_inv coeIdeal_le_one
coe_ideal_span_singleton_div_self 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors coeIdeal Ideal.span Set Set.instSingletonSet instOne	—	coeIdeal_span_singleton spanSingleton_div_self map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective IsFractionRing.instFaithfulSMul
coe_ideal_span_singleton_inv_mul 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors coeIdeal Ideal.span Set Set.instSingletonSet instOne	—	mul_comm coe_ideal_span_singleton_mul_inv
coe_ideal_span_singleton_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul coeIdeal Ideal.span Set Set.instSingletonSet instInvNonZeroDivisors instOne	—	coeIdeal_span_singleton spanSingleton_mul_inv map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective IsFractionRing.instFaithfulSMul
coe_inv_of_ne_zero 📖	mathematical	—	coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instInvNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semifield.toCommSemiring Field.toSemifield Algebra.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.instDiv IsLocalization.coeSubmodule Top.top Ideal Submodule.instTop Semiring.toModule	—	isFractional_div_of_ne_zero inv_of_ne_zero coe_one IsLocalization.coeSubmodule_top
coe_inv_of_nonzero 📖	mathematical	—	coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing FractionalIdeal instInvNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semifield.toCommSemiring Field.toSemifield Algebra.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.instDiv IsLocalization.coeSubmodule Top.top Ideal Submodule.instTop Semiring.toModule	—	coe_inv_of_ne_zero
den_mem_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing SetLike.instMembership instSetLike instInvNonZeroDivisors DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike den	—	mem_inv_iff Algebra.smul_def mem_coe coe_one RingHomSurjective.ids le_trans Submodule.map_mono Ideal.one_eq_top Submodule.map_top Submodule.one_eq_range le_refl smulCommClass_self Submodule.smul_mem_pointwise_smul Submonoid.smulCommClass_left den_mul_self_eq_num
inv_anti_mono 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	instInvNonZeroDivisors	—	mem_inv_iff
inv_eq 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instInvNonZeroDivisors instDivNonZeroDivisors instOne	—	—
inv_nonzero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instInvNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule IsFractional Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule instOne isFractional_div_of_ne_zero	—	inv_of_ne_zero
inv_of_ne_zero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instInvNonZeroDivisors Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule IsFractional Submodule.instDiv Semifield.toCommSemiring Field.toSemifield coeToSubmodule instOne isFractional_div_of_ne_zero	—	div_of_ne_zero
inv_zero' 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instInvNonZeroDivisors instZero	—	div_zero
invertible_iff_generator_nonzero 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors instOne	—	ne_zero_of_mul_eq_one eq_spanSingleton_of_principal spanSingleton_zero invertible_of_principal mem_spanSingleton_self mem_zero_iff
invertible_of_principal 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors instOne	—	mul_div_self_cancel_iff mul_generator_self_inv
isPrincipal_inv 📖	mathematical	—	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Submodule IsFractional nonZeroDivisors Semiring.toMonoidWithZero FractionalIdeal instInvNonZeroDivisors	—	val_eq_coe isPrincipal_iff mul_generator_self_inv right_inverse_eq
le_self_mul_inv 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder instOne	instMul instInvNonZeroDivisors	—	le_self_mul_one_div
map_inv 📖	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 instInvNonZeroDivisors	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass inv_eq map_div map_one
mem_inv_iff 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing SetLike.instMembership instSetLike instInvNonZeroDivisors instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mem_div_iff_of_ne_zero
mul_generator_self_inv 📖	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 Submodule.IsPrincipal.generator NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule coeToSubmodule instOne	—	eq_spanSingleton_of_principal spanSingleton_mul_spanSingleton mul_inv_cancel₀ spanSingleton_zero spanSingleton_one
mul_inv_cancel_iff 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors instOne	—	right_inverse_eq
mul_inv_cancel_iff_isUnit 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors instOne IsUnit MonoidWithZero.toMonoid commSemiring	—	mul_inv_cancel_iff isUnit_iff_exists_inv instIsDedekindFiniteMonoid
num_le_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing Preorder.toLE PartialOrder.toPreorder instPartialOrder coeIdeal num instMul instInvNonZeroDivisors	—	num_zero_eq FaithfulSMul.algebraMap_injective IsFractionRing.instFaithfulSMul MulZeroClass.zero_mul Submodule.zero_eq_bot coeIdeal_bot le_refl mul_comm den_mul_self_eq_num' mul_le_mul_left instMulRightMono spanSingleton_le_iff_mem den_mem_inv
right_inverse_eq 📖	mathematical	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instOne	instInvNonZeroDivisors	—	eq_one_div_of_mul_eq_one_right
spanSingleton_div_self 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors spanSingleton instOne	—	spanSingleton_div_spanSingleton div_self spanSingleton_one
spanSingleton_div_spanSingleton 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instDivNonZeroDivisors spanSingleton DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_spanSingleton mul_comm spanSingleton_mul_spanSingleton div_eq_mul_inv
spanSingleton_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instInvNonZeroDivisors spanSingleton InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	one_div_spanSingleton
spanSingleton_inv_mul 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul instInvNonZeroDivisors spanSingleton instOne	—	mul_comm spanSingleton_mul_inv
spanSingleton_mul_inv 📖	mathematical	—	FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing instMul spanSingleton instInvNonZeroDivisors instOne	—	spanSingleton_inv spanSingleton_mul_spanSingleton mul_inv_cancel₀ spanSingleton_one

---

← Back to Index