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`, `den_mem_inv`, `inv_anti_mono`, `inv_eq`, `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`	27
Total	29

FractionalIdeal

Definitions

Name	Category	Theorems
`instInvNonZeroDivisors` 📖	CompOp	40 math math: `spanSingleton_inv_mul`, `spanSingleton_mul_inv`, `inv_anti_mono`, `mul_inv_cancel_of_le_one`, `invertible_of_principal`, `inv_le_inv_iff`, `right_inverse_eq`, `le_self_mul_inv`, `inv_eq`, `differentialIdeal_le_iff`, `coeIdeal_differentIdeal`, `inv_le_dual`, `le_inv_comm`, `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`, `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`
`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`	`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_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`	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `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`	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `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