Instances

📁 Source: Mathlib/RingTheory/DedekindDomain/Instances.lean

Statistics

Metric	Count
Definitions algebra_localization_localization, liftAlgebra, instAlgebraAtPrimeFractionRing	3
Theorems isSeparable_of_isLocalization, algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, instIsFractionRingAtPrimeFractionRing, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, instIsScalarTowerAtPrimeFractionRing, instIsScalarTowerAtPrimeFractionRing_1, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2	21
Total	24

FractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_of_isLocalization 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Algebra.IsSeparable FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instRing CommRing.toRing	—	instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial IsScalarTower.right algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul IsDomain.to_noZeroDivisors Localization.isLocalization IsLocalization.localization_isScalarTower_of_submonoid_le IsFractionRing.isFractionRing_of_isDomain_of_isLocalization IsLocalization.isDomain_of_le_nonZeroDivisors Algebra.IsSeparable.of_equiv_equiv IsLocalization.ringHom_ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.ext AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass instIsScalarTower OreLocalization.instIsScalarTower IsScalarTower.left IsScalarTower.algebraMap_apply AlgEquiv.coe_ringEquiv AlgEquiv.commutes

Localization.AtPrime

Definitions

Name	Category	Theorems
algebra_localization_localization 📖	CompOp	6 math math: instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1
liftAlgebra 📖	CompOp	3 math math: instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing

(root)

Definitions

Name	Category	Theorems
instAlgebraAtPrimeFractionRing 📖	CompOp	3 math math: instIsScalarTowerAtPrimeFractionRing_1, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instIsScalarTowerAtPrimeFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Algebra.algebraMapSubmonoid	—	map_le_nonZeroDivisors_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective
instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Module.Finite Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule Algebra.toModule OreLocalization.instCommSemiring Localization.AtPrime.algebra_localization_localization	—	Module.Finite.of_isLocalization OreLocalization.instIsScalarTower IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl Localization.isLocalization instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization
instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	IsDedekindDomain Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instCommRing OreLocalization.oreSetComm	—	IsLocalization.isDedekindDomain algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul IsDomain.to_noZeroDivisors Ideal.primeCompl_le_nonZeroDivisors IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul Localization.isLocalization
instIsFractionRingAtPrimeFractionRing 📖	mathematical	—	IsFractionRing Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid FractionRing nonZeroDivisors Semiring.toMonoidWithZero CommRing.toCommMonoid IsLocalization.instAlgebraLocalizationAtPrime	—	IsFractionRing.isFractionRing_of_isDomain_of_isLocalization IsLocalization.instIsScalarTowerAtPrimeFractionRing Localization.isLocalization
instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing 📖	mathematical	—	IsFractionRing Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instCommSemiring OreLocalization.oreSetComm FractionRing nonZeroDivisors Semiring.toMonoidWithZero Localization.AtPrime.liftAlgebra	—	IsFractionRing.isFractionRing_of_isDomain_of_isLocalization instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing Localization.isLocalization
instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Algebra.IsIntegral Localization.AtPrime CommRing.toCommSemiring Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instCommRing OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instRing CommRing.toRing instAlgebraLocalizationAlgebraMapSubmonoid	—	Algebra.isIntegral_def Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map isIntegral_localization IsLocalization.algebraMap_eq_map_map_submonoid instIsScalarTowerLocalizationAlgebraMapSubmonoid OreLocalization.instIsScalarTower IsScalarTower.right
instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization 📖	mathematical	—	IsLocalization CommRing.toCommSemiring Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl Localization CommRing.toCommMonoid OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id	—	Algebra.algebraMapSubmonoid_map_map Localization.isLocalization
instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal 📖	mathematical	—	IsPrincipalIdealRing Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSemiring OreLocalization.oreSetComm	—	IsDedekindDomain.isPrincipalIdealRing_localization_over_prime FaithfulSMul.to_isTorsionFree IsDomain.toNontrivial IsDomain.toIsCancelMulZero Localization.isLocalization OreLocalization.instIsScalarTower IsScalarTower.right instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl
instIsScalarTowerAtPrimeFractionRing 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring FractionRing Algebra.toSMul OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero CommRing.toCommMonoid instAlgebraAtPrimeFractionRing Algebra.id Module.Free.instFaithfulSMulOfNontrivial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Free.self IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield FractionRing.field FractionRing.liftAlgebra OreLocalization.instAlgebra FractionRing.instFaithfulSMul	—	IsScalarTower.of_algebraMap_eq' Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial FractionRing.instFaithfulSMul IsLocalization.ringHom_ext Localization.isLocalization RingHom.ext IsLocalization.lift_comp IsLocalization.lift_eq IsFractionRing.lift_algebraMap
instIsScalarTowerAtPrimeFractionRing_1 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring FractionRing OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero CommRing.toCommMonoid instAlgebraAtPrimeFractionRing Module.Free.instFaithfulSMulOfNontrivial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Free.self IsDomain.toNontrivial	—	IsScalarTower.of_algebraMap_eq' Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial RingHom.ext IsLocalization.lift_comp
instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl Algebra.toSMul OreLocalization.instCommSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instSemiring instAlgebraLocalizationAlgebraMapSubmonoid Localization.AtPrime.algebra_localization_localization	—	Localization.ind nonZeroDivisors.ne_zero IsDomain.toNontrivial Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors Subtype.prop IsScalarTower.right instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1 Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero smul_assoc instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1 instIsScalarTowerLocalizationAlgebraMapSubmonoid smul_eq_mul Localization.isLocalization Localization.mk_eq_mk' IsLocalization.mk'_mul_cancel_left IsScalarTower.algebraMap_smul
instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl FractionRing Algebra.toSMul OreLocalization.instCommSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instSemiring instAlgebraLocalizationAlgebraMapSubmonoid nonZeroDivisors Semiring.toMonoidWithZero Localization.AtPrime.liftAlgebra instAlgebraAtPrimeFractionRing	—	IsScalarTower.of_algebraMap_eq' IsLocalization.ringHom_ext Localization.isLocalization RingHom.comp_assoc IsScalarTower.algebraMap_eq instIsScalarTowerLocalizationAlgebraMapSubmonoid OreLocalization.instIsScalarTower IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial instIsScalarTowerAtPrimeFractionRing instIsScalarTowerAtPrimeFractionRing_1 FractionRing.instIsScalarTower IsScalarTower.left
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	IsScalarTower Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring Localization.AtPrime.algebra_localization_localization	—	IsScalarTower.of_algebraMap_eq' instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization RingHom.algebraMap_toAlgebra IsLocalization.map_comp IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing 📖	mathematical	—	IsScalarTower Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl FractionRing OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero Localization.AtPrime.liftAlgebra	—	IsLocalization.localization_isScalarTower_of_submonoid_le algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul IsDomain.to_noZeroDivisors Ideal.primeCompl_le_nonZeroDivisors Localization.isLocalization
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1 📖	mathematical	—	IsScalarTower Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring Localization.AtPrime.algebra_localization_localization	—	IsScalarTower.of_algebraMap_eq' IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right RingHom.comp_assoc instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl
instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Algebra.IsSeparable FractionRing Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.instRing CommRing.toRing FractionRing.liftAlgebra FractionRing.field IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul OreLocalization.instAlgebra OreLocalization.instCommSemiring instAlgebraLocalizationAlgebraMapSubmonoid FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero OreLocalization.instSemiring IsLocalization.isDomain_of_local_atPrime IsDomain.toNontrivial Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain FaithfulSMul.to_isTorsionFree	—	FractionRing.instFaithfulSMul FractionRing.isSeparable_of_isLocalization FaithfulSMul.to_isTorsionFree IsDomain.toNontrivial IsDomain.toIsCancelMulZero Localization.isLocalization instIsScalarTowerLocalizationAlgebraMapSubmonoid OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsLocalization.isDomain_of_local_atPrime Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain FractionRing.instIsScalarTower IsScalarTower.left Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors
instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Algebra.IsSeparable FractionRing Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instCommRing OreLocalization.oreSetComm nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.instRing CommRing.toRing FractionRing.liftAlgebra FractionRing.field IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial OreLocalization.instAlgebra Localization.AtPrime.algebra_localization_localization FractionRing.instFaithfulSMul OreLocalization.instSemiring instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2	—	FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial FractionRing.isSeparable_of_isLocalization Localization.isLocalization instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl OreLocalization.instIsScalarTower IsScalarTower.right instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2 FractionRing.instIsScalarTower IsScalarTower.left algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul IsDomain.to_noZeroDivisors mem_nonZeroDivisors_of_ne_zero AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl 📖	mathematical	—	Module.IsTorsionFree Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule OreLocalization.instModuleOfIsScalarTower NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.right Algebra.id	—	IsScalarTower.right Module.isTorsionFree_iff_algebraMap_injective IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul IsLocalization.injective_iff_isRegular Localization.isLocalization isRegular_iff_ne_zero' IsDomain.toNontrivial IsDomain.to_noZeroDivisors AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1 📖	mathematical	—	Module.IsTorsionFree Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule OreLocalization.instModuleOfIsScalarTower NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IsScalarTower.right	—	IsLocalization.AtPrime.faithfulSMul IsDomain.to_noZeroDivisors Localization.isLocalization Module.IsTorsionFree.trans_faithfulSMul IsDomain.toNontrivial IsDomain.toIsCancelMulZero IsLocalization.isDomain_of_local_atPrime IsScalarTower.right Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain FaithfulSMul.to_isTorsionFree instIsScalarTowerLocalizationAlgebraMapSubmonoid
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2 📖	mathematical	—	Module.IsTorsionFree Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommRing.toCommSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule Algebra.toModule OreLocalization.instCommSemiring Localization.AtPrime.algebra_localization_localization	—	Module.IsTorsionFree.of_isLocalization IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul OreLocalization.instIsScalarTower IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul IsDomain.to_noZeroDivisors Ideal.primeCompl_le_nonZeroDivisors Localization.isLocalization instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization

---

← Back to Index