Extended

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

Statistics

Metric	Count
Definitions `extended`, `extendedHom`, `extendedHomₐ`	3
Theorems `coe_extendedHomₐ_eq_span`, `coe_extended_eq_span`, `extendedHom_apply`, `extendedHomₐ_coeIdeal_eq_map`, `extendedHomₐ_eq_one_iff`, `extendedHomₐ_eq_zero_iff`, `extendedHomₐ_injective`, `extendedHomₐ_le_one_iff`, `extended_add`, `extended_coeIdeal_eq_map`, `extended_eq_zero_iff`, `extended_le_one_of_le_one`, `extended_mul`, `extended_ne_zero`, `extended_one`, `extended_zero`, `le_one_of_extendedHomₐ_le_one`, `mem_extended_iff`, `one_le_extendedHomₐ_iff`, `one_le_extended_of_one_le`	20
Total	23

FractionalIdeal

Definitions

Name	Category	Theorems
`extended` 📖	CompOp	11 math math: `extendedHom_apply`, `extended_le_one_of_le_one`, `extended_zero`, `one_le_extended_of_one_le`, `extended_coeIdeal_eq_map`, `extended_mul`, `extended_one`, `extended_add`, `mem_extended_iff`, `extended_eq_zero_iff`, `coe_extended_eq_span`
`extendedHom` 📖	CompOp	1 math math: `extendedHom_apply`
`extendedHomₐ` 📖	CompOp	8 math math: `coe_extendedHomₐ_eq_span`, `extendedHomₐ_coeIdeal_eq_map`, `dual_eq_dual_mul_dual`, `extendedHomₐ_injective`, `extendedHomₐ_eq_zero_iff`, `extendedHomₐ_eq_one_iff`, `one_le_extendedHomₐ_iff`, `extendedHomₐ_le_one_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_extendedHomₐ_eq_span` 📖	mathematical	—	`coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `FractionalIdeal` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Set.image` `Semifield.toCommSemiring` `algebraMap` `SetLike.coe` `instSetLike`	—	`extendedHom_apply` `coe_extended_eq_span` `Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Algebra.IsIntegral.isAlgebraic` `IsDomain.to_noZeroDivisors` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.le_comap_map` `IsLocalization.algebraMap_eq_map_map_submonoid`
`coe_extended_eq_span` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`coeToSubmodule` `extended` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Set.image` `DFunLike.coe` `IsLocalization.map` `SetLike.coe` `FractionalIdeal` `instSetLike`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submodule.ext`
`extendedHom_apply` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`DFunLike.coe` `FractionalIdeal` `commSemiring` `extendedHom` `extended`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`extendedHomₐ_coeIdeal_eq_map` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `coeIdeal` `Ideal.map` `algebraMap`	—	`extended_coeIdeal_eq_map`
`extendedHomₐ_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `instOne`	—	`le_antisymm_iff` `extendedHomₐ_le_one_iff` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `one_le_extendedHomₐ_iff`
`extendedHomₐ_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `instZero`	—	`extended_eq_zero_iff` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `zero_notMem_nonZeroDivisors`
`extendedHomₐ_injective` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ`	—	`extendedHomₐ_eq_zero_iff` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_inv_eq_one₀` `extendedHomₐ_eq_one_iff` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `inv_ne_zero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_inv₀` `Iff.not`
`extendedHomₐ_le_one_iff` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `instOne`	—	`le_one_of_extendedHomₐ_le_one` `extended_le_one_of_le_one`
`extended_add` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`extended` `FractionalIdeal` `instAdd`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeToSubmodule_injective` `coe_extended_eq_span` `Submodule.span_eq_span` `mem_add` `SetLike.mem_coe` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.subset_span` `Set.mem_union_left` `Set.mem_union_right` `zero_mem` `add_zero` `zero_add`
`extended_coeIdeal_eq_map` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`extended` `coeIdeal` `Ideal.map`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ideal.map.eq_1` `Ideal.span.eq_1` `Ideal.submodule_span_eq` `coe_coeIdeal` `IsLocalization.coeSubmodule_span` `coe_extended_eq_span` `Submodule.span_eq_span` `Submodule.subset_span` `Set.mem_image_of_mem` `Algebra.linearMap_apply` `IsLocalization.map_eq` `mem_coeIdeal_of_mem`
`extended_eq_zero_iff` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `DFunLike.coe` `SetLike.instMembership` `Submonoid.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`extended` `FractionalIdeal` `instZero`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Mathlib.Tactic.Contrapose.contrapose₁` `extended_ne_zero` `extended_zero`
`extended_le_one_of_le_one` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FractionalIdeal` `instPartialOrder` `instOne`	`extended`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `le_one_iff_exists_coeIdeal` `Submodule.sum_smul_mem` `IsLocalization.map_eq`
`extended_mul` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`extended` `FractionalIdeal` `instMul`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeToSubmodule_injective` `coe_extended_eq_span` `IsScalarTower.right` `coe_mul` `Submodule.span_mul_span` `Submodule.span_eq_span` `Submodule.span_induction` `Set.mem_mul` `Submodule.subset_span` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.add_mem` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Algebra.smul_def` `IsLocalization.map_eq` `Submodule.smul_mem` `Submodule.mul_eq_span_mul_set` `mul_mem_mul`
`extended_ne_zero` 📖	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `DFunLike.coe` `SetLike.instMembership` `Submonoid.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coe_extended_eq_span` `coe_zero` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `IsLocalization.map_injective_of_injective'`
`extended_one` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`extended` `FractionalIdeal` `instOne`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeToSubmodule_injective` `Submodule.ext` `Submodule.span_induction` `Algebra.linearMap_apply` `IsLocalization.map_eq` `zero_mem` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `Algebra.algebraMap_eq_smul_one` `Submodule.subset_span` `map_one` `MonoidHomClass.toOneHomClass` `one_mem_one`
`extended_zero` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`extended` `FractionalIdeal` `instZero`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Set.ext` `coeToSubmodule_injective` `coe_extended_eq_span` `Set.image_singleton` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Submodule.span_zero_singleton` `coe_zero`
`le_one_of_extendedHomₐ_le_one` 📖	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ` `instOne`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `SetLike.not_le_iff_exists` `instIsConcreteLE` `Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Algebra.IsIntegral.isAlgebraic` `IsDomain.to_noZeroDivisors` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.le_comap_map` `IsLocalization.algebraMap_eq_map_map_submonoid` `coe_extended_eq_span` `Submodule.subset_span` `Set.mem_image_of_mem` `Mathlib.Tactic.Contrapose.contrapose₄` `mem_one_iff` `IsIntegrallyClosed.isIntegral_iff` `IsIntegral.tower_bot_of_field` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isIntegral_trans`
`mem_extended_iff` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	`FractionalIdeal` `SetLike.instMembership` `instSetLike` `extended` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `IsLocalization.map` `SetLike.coe`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`one_le_extendedHomₐ_iff` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ`	—	`IsDedekindDomain.toIsDomain` `inv_le_inv_iff` `Iff.not` `extendedHomₐ_eq_zero_iff` `NeZero.one` `instNontrivialNonZeroDivisors` `inv_one` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `extendedHomₐ_le_one_iff` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `inv_le_comm`
`one_le_extended_of_one_le` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FractionalIdeal` `instPartialOrder` `instOne`	`extended`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_le` `mem_extended_iff` `Submodule.subset_span` `map_one` `MonoidHomClass.toOneHomClass`

---

← Back to Index