FractionRing

📁 Source: Mathlib/RingTheory/Localization/FractionRing.lean

Statistics

Metric	Count
Definitions FractionRing, algEquiv, instDecidableEq, liftAlgebra, unique, IsFractionRing, algEquiv, algEquivOfAlgEquiv, fieldEquivOfAlgEquiv, fieldEquivOfAlgEquivHom, inv, liftAlgHom, map, ringEquivOfRingEquiv, toField	15
Theorems of_field_isFractionRing, algebraMap_liftAlgebra, instFaithfulSMul, instIsFractionRing, instIsScalarTower, instIsScalarTower_1, instNontrivial, isScalarTower_liftAlgebra, mk_eq_div, algEquivOfAlgEquiv_algebraMap, algEquivOfAlgEquiv_symm, algEquiv_commutes, algHom_commutes, closure_range_algebraMap, coe_inj, coe_liftAlgHom, div_surjective, fieldEquivOfAlgEquivHom_apply, fieldEquivOfAlgEquivHom_injective, fieldEquivOfAlgEquiv_algebraMap, fieldEquivOfAlgEquiv_refl, fieldEquivOfAlgEquiv_trans, idem, injective, injective_comp_algebraMap, instFaithfulSMul, inv_def, isDomain, isFractionRing_iff_of_base_ringEquiv, isUnit_map_of_injective, liftAlgHom_apply, liftAlgHom_toRingHom, lift_algebraMap, lift_fieldRange, lift_fieldRange_eq_of_range_eq, lift_mk', lift_unique, mk'_eq_div, mk'_eq_one_iff_eq, mk'_eq_zero_iff_eq_zero, mk'_mk_eq_div, mul_inv_cancel, nonZeroDivisors_eq_isUnit, nontrivial, nontrivial_iff_nontrivial, of_field, of_ringEquiv_left, restrictScalars_fieldEquivOfAlgEquiv, ringEquivOfRingEquiv_algebraMap, ringEquivOfRingEquiv_symm, ringHom_ext, ringHom_fieldRange_eq_of_comp_eq, ringHom_fieldRange_eq_of_comp_eq_of_range_eq, self_iff_bijective, self_iff_nonZeroDivisors_eq_isUnit, self_iff_nonZeroDivisors_le_isUnit, self_iff_surjective, surjective_iff_isField, to_map_eq_zero_iff, to_map_ne_zero_of_mem_nonZeroDivisors, trans, isFractionRing, isFractionRing, algebraMap_injective_of_field_isFractionRing, instIsFractionRing, instIsLocalizationIntPosRat	66
Total	81

FaithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_field_isFractionRing 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	faithfulSMul_iff_algebraMap_injective algebraMap_injective_of_field_isFractionRing

FractionRing

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	1 math math: map_equiv_traceDual
instDecidableEq 📖	CompOp	—
liftAlgebra 📖	CompOp	23 math math: instIsScalarTower, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, algebraMap_liftAlgebra, instIsPushoutFractionRingPolynomial_1, coeSubmodule_differentIdeal_fractionRing, Algebra.algebraMap_intNorm_fractionRing, instIsScalarTower_1, instIsScalarTowerAtPrimeFractionRing, map_equiv_traceDual, Ideal.relNorm_algebraMap', Ideal.relNorm_algebraMap, IsGaloisGroup.toFractionRing, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Algebra.IsAlgebraic.rank_fractionRing, instIsPushoutFractionRingPolynomial, isScalarTower_liftAlgebra, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, Algebra.algebraMap_intTrace_fractionRing, Ideal.absNorm_algebraMap, instFiniteDimensionalFractionRingOfFinite, Algebra.IsAlgebraic.rank_fractionRing_polynomial, instIsPushoutFractionRingMvPolynomial_1, instIsPushoutFractionRingMvPolynomial
unique 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_liftAlgebra 📖	mathematical	—	algebraMap FractionRing OreLocalization.instCommSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommRing.toCommMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield liftAlgebra IsFractionRing.lift field IsDomain.of_faithfulSMul instIsDomain OreLocalization.instAlgebra Algebra.id Localization.isLocalization FaithfulSMul.algebraMap_injective	—	—
instFaithfulSMul 📖	mathematical	—	FaithfulSMul FractionRing OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul IsScalarTower.right	—	IsScalarTower.right faithfulSMul_iff_algebraMap_injective IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower FaithfulSMul.algebraMap_injective IsFractionRing.instFaithfulSMul Localization.isLocalization
instIsFractionRing 📖	mathematical	—	IsFractionRing FractionRing OreLocalization.instCommSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id	—	IsFractionRing.idem Localization.isLocalization
instIsScalarTower 📖	mathematical	—	IsScalarTower FractionRing OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul OreLocalization.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield liftAlgebra	—	IsScalarTower.to₁₃₄ IsScalarTower.right OreLocalization.instIsScalarTower isScalarTower_liftAlgebra
instIsScalarTower_1 📖	mathematical	—	IsScalarTower FractionRing Algebra.toSMul OreLocalization.instCommSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommRing.toCommMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield liftAlgebra Semifield.toCommSemiring	—	Localization.ind FaithfulSMul.to_isTorsionFree IsDomain.toNontrivial IsDomain.toIsCancelMulZero instIsDomain nonZeroDivisors.coe_ne_zero IsScalarTower.right instIsScalarTower IsScalarTower.left Localization.isLocalization Localization.mk_eq_mk' IsLocalization.mk'_mul_cancel_left algebraMap_smul smul_assoc
instNontrivial 📖	mathematical	—	Nontrivial FractionRing	—	OreLocalization.nontrivial
isScalarTower_liftAlgebra 📖	mathematical	—	IsScalarTower FractionRing OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield liftAlgebra	—	IsDomain.of_faithfulSMul instIsDomain IsScalarTower.of_algebraMap_eq FaithfulSMul.algebraMap_injective IsFractionRing.lift_algebraMap
mk_eq_div 📖	mathematical	—	CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid OreLocalization.instDivisionRingNonZeroDivisors CommRing.toRing IsDomain.toNontrivial IsDomain.to_noZeroDivisors OreLocalization.oreSetComm DFunLike.coe RingHom Semiring.toNonAssocSemiring OreLocalization.instSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors Localization.isLocalization Localization.mk_eq_mk' IsFractionRing.mk'_eq_div

IsFractionRing

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	—
algEquivOfAlgEquiv 📖	CompOp	3 math math: restrictScalars_fieldEquivOfAlgEquiv, algEquivOfAlgEquiv_algebraMap, algEquivOfAlgEquiv_symm
fieldEquivOfAlgEquiv 📖	CompOp	5 math math: fieldEquivOfAlgEquivHom_apply, fieldEquivOfAlgEquiv_trans, fieldEquivOfAlgEquiv_refl, fieldEquivOfAlgEquiv_algebraMap, restrictScalars_fieldEquivOfAlgEquiv
fieldEquivOfAlgEquivHom 📖	CompOp	2 math math: fieldEquivOfAlgEquivHom_apply, fieldEquivOfAlgEquivHom_injective
inv 📖	CompOp	2 math math: inv_def, mul_inv_cancel
liftAlgHom 📖	CompOp	6 math math: coe_liftAlgHom, liftAlgHom_fieldRange_eq_of_range_eq, AlgebraicIndependent.liftAlgHom_comp_reprField, liftAlgHom_toRingHom, liftAlgHom_fieldRange, liftAlgHom_apply
map 📖	CompOp	—
ringEquivOfRingEquiv 📖	CompOp	4 math math: ringEquivOfRingEquiv_algebraMap, WittVector.exists_frobenius_solution_fractionRing, ringEquivOfRingEquiv_symm, WittVector.exists_frobenius_solution_fractionRing_aux
toField 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquivOfAlgEquiv_algebraMap 📖	mathematical	—	DFunLike.coe AlgEquiv CommSemiring.toSemiring CommRing.toCommSemiring AlgEquiv.instFunLike algEquivOfAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsLocalization.map_eq AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
algEquivOfAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm CommSemiring.toSemiring CommRing.toCommSemiring algEquivOfAlgEquiv	—	—
algEquiv_commutes 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap AlgEquiv CommRing.toCommSemiring AlgEquiv.instFunLike	—	algHom_commutes
algHom_commutes 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap AlgHom CommRing.toCommSemiring AlgHom.funLike	—	div_surjective map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass AlgHom.commutes IsScalarTower.algebraMap_apply
closure_range_algebraMap 📖	mathematical	—	Subfield.closure Field.toDivisionRing Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Top.top Subfield Subfield.instTop	—	top_unique div_surjective div_mem SubfieldClass.toSubgroupClass Subfield.instSubfieldClass Subfield.subset_closure
coe_inj 📖	mathematical	—	Algebra.cast CommRing.toCommSemiring CommSemiring.toSemiring	—	instFaithfulSMul
coe_liftAlgHom 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	DFunLike.coe AlgHom CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike liftAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike lift AlgHom.toRingHom CommSemiring.toSemiring	—	—
div_surjective 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	IsLocalization.exists_mk'_eq mk'_eq_div
fieldEquivOfAlgEquivHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MonoidHom.instFunLike fieldEquivOfAlgEquivHom fieldEquivOfAlgEquiv	—	—
fieldEquivOfAlgEquivHom_injective 📖	mathematical	—	AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MonoidHom.instFunLike fieldEquivOfAlgEquivHom	—	AlgEquiv.ext fieldEquivOfAlgEquiv_algebraMap instFaithfulSMul AlgEquiv.ext_iff
fieldEquivOfAlgEquiv_algebraMap 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike fieldEquivOfAlgEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	ringEquivOfRingEquiv_algebraMap
fieldEquivOfAlgEquiv_refl 📖	mathematical	—	fieldEquivOfAlgEquiv AlgEquiv.refl CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	AlgEquiv.ext div_surjective map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass fieldEquivOfAlgEquiv_algebraMap
fieldEquivOfAlgEquiv_trans 📖	mathematical	—	fieldEquivOfAlgEquiv AlgEquiv.trans CommRing.toCommSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	AlgEquiv.ext div_surjective map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass fieldEquivOfAlgEquiv_algebraMap
idem 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Algebra.id	—	IsLocalization.self Eq.le nonZeroDivisors_eq_isUnit
injective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.injective le_of_eq
injective_comp_algebraMap 📖	mathematical	—	RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring RingHom.comp algebraMap	—	ringHom_ext RingHom.congr_fun
instFaithfulSMul 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	faithfulSMul_iff_algebraMap_injective injective
inv_def 📖	mathematical	—	inv MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike IsLocalization.sec	—	—
isDomain 📖	mathematical	—	IsDomain CommSemiring.toSemiring CommRing.toCommSemiring	—	IsLocalization.isDomain_of_le_nonZeroDivisors le_refl
isFractionRing_iff_of_base_ringEquiv 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring RingHom.toAlgebra RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring algebraMap RingEquiv.toRingHom RingEquiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass MulEquivClass.toMonoidWithZeroHomClass RingEquivClass.toMulEquivClass MulEquivClass.map_nonZeroDivisors IsLocalization.isLocalization_iff_of_base_ringEquiv
isUnit_map_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	map_ne_zero_of_mem_nonZeroDivisors RingHom.domain_nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
liftAlgHom_apply 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	DFunLike.coe AlgHom CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike liftAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike lift AlgHom.toRingHom CommSemiring.toSemiring	—	—
liftAlgHom_toRingHom 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	AlgHom.toRingHom CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield liftAlgHom lift CommSemiring.toSemiring	—	—
lift_algebraMap 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike lift CommSemiring.toSemiring CommRing.toCommSemiring algebraMap	—	IsLocalization.lift_eq isUnit_map_of_injective
lift_fieldRange 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	RingHom.fieldRange Field.toDivisionRing lift Subfield.closure SetLike.coe Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Field.toCommRing Subring.instSetLike RingHom.range	—	ringHom_fieldRange_eq_of_comp_eq RingHom.ext lift_algebraMap
lift_fieldRange_eq_of_range_eq 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike RingHom.range NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Field.toCommRing Subring.closure	RingHom.fieldRange Field.toDivisionRing lift Subfield.closure	—	ringHom_fieldRange_eq_of_comp_eq_of_range_eq RingHom.ext lift_algebraMap
lift_mk' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike lift IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	mk'_eq_div map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lift_algebraMap
lift_unique 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	lift	—	IsLocalization.lift_unique isUnit_map_of_injective
mk'_eq_div 📖	mathematical	—	IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	mk'_mk_eq_div
mk'_eq_one_iff_eq 📖	mathematical	—	IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	to_map_ne_zero_of_mem_nonZeroDivisors RingHom.domain_nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing injective div_eq_one_iff_eq mk'_eq_div IsLocalization.mk'_self'
mk'_eq_zero_iff_eq_zero 📖	mathematical	—	IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	mk'_eq_div instFaithfulSMul IsSimpleRing.instNontrivial DivisionRing.isSimpleRing IsDomain.to_noZeroDivisors instIsDomain RingHom.domain_nontrivial
mk'_mk_eq_div 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	IsLocalization.mk'_eq_iff_eq_mul div_mul_cancel₀ to_map_ne_zero_of_mem_nonZeroDivisors RingHom.domain_nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
mul_inv_cancel 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing inv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	inv_def mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial IsLocalization.eq_zero_of_fst_eq_zero IsLocalization.sec_spec IsLocalization.map_units one_mul mul_assoc IsLocalization.mk'_spec IsLocalization.eq_mk'_iff_mul_eq IsLocalization.mk'_sec
nonZeroDivisors_eq_isUnit 📖	mathematical	—	nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring IsUnit.submonoid MonoidWithZero.toMonoid	—	le_antisymm IsLocalization.surj mem_nonZeroDivisors_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass injective MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass IsUnit.mem_nonZeroDivisors IsLocalization.map_units isUnit_of_mul_isUnit_left instIsDedekindFiniteMonoid isUnit_le_nonZeroDivisors
nontrivial 📖	mathematical	—	Nontrivial	—	nontrivial_iff_nontrivial
nontrivial_iff_nontrivial 📖	mathematical	—	Nontrivial	—	IsLocalization.exists_of_eq mul_one MulZeroClass.mul_zero IsUnit.ne_zero IsLocalization.map_units Subsingleton.eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
of_field 📖	mathematical	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	IsFractionRing CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield	—	FaithfulSMul.algebraMap_injective Function.Injective.noZeroDivisors map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsDomain.to_noZeroDivisors instIsDomain Module.nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing map_ne_zero_iff mem_nonZeroDivisors_iff_ne_zero eq_or_ne map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass mul_one div_zero eq_div_iff_mul_eq one_mul
of_ringEquiv_left 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	IsFractionRing	—	IsLocalization.of_ringEquiv_left MulEquivClass.map_nonZeroDivisors RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass
restrictScalars_fieldEquivOfAlgEquiv 📖	mathematical	—	AlgEquiv.restrictScalars CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring fieldEquivOfAlgEquiv algEquivOfAlgEquiv Field.toCommRing	—	AlgEquiv.ext
ringEquivOfRingEquiv_algebraMap 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivOfRingEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.map_eq
ringEquivOfRingEquiv_symm 📖	mathematical	—	RingEquiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd ringEquivOfRingEquiv	—	—
ringHom_ext 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike CommSemiring.toSemiring CommRing.toCommSemiring algebraMap	—	—	RingHom.ext div_surjective map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ringHom_fieldRange_eq_of_comp_eq 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield algebraMap	RingHom.fieldRange Field.toDivisionRing Subfield.closure SetLike.coe Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Field.toCommRing Subring.instSetLike RingHom.range	—	RingHom.fieldRange_eq_map closure_range_algebraMap RingHom.map_field_closure Set.range_comp RingHom.coe_comp RingHom.coe_range
ringHom_fieldRange_eq_of_comp_eq_of_range_eq 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield algebraMap RingHom.range NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Field.toCommRing Subring.closure	RingHom.fieldRange Field.toDivisionRing Subfield.closure	—	ringHom_fieldRange_eq_of_comp_eq Subfield.ext Subring.closure_eq
self_iff_bijective 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Algebra.id Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	AlgEquiv.bijective self_iff_nonZeroDivisors_le_isUnit IsLocalization.isLocalization_of_algEquiv
self_iff_nonZeroDivisors_eq_isUnit 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Algebra.id nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring IsUnit.submonoid MonoidWithZero.toMonoid	—	nonZeroDivisors_eq_isUnit IsLocalization.self Eq.le
self_iff_nonZeroDivisors_le_isUnit 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Algebra.id Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors IsUnit.submonoid MonoidWithZero.toMonoid	—	self_iff_nonZeroDivisors_eq_isUnit le_antisymm_iff isUnit_le_nonZeroDivisors
self_iff_surjective 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Algebra.id DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	self_iff_bijective Function.Bijective.eq_1 injective
surjective_iff_isField 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap IsField	—	MulEquiv.isField Field.toIsField RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass injective AlgEquiv.surjective Ne.isUnit mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
to_map_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsLocalization.to_map_eq_zero_iff le_rfl
to_map_ne_zero_of_mem_nonZeroDivisors 📖	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	—	IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors le_rfl
trans 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring	—	IsLocalization.isLocalization_of_algEquiv IsScalarTower.right

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFractionRing 📖	mathematical	—	IsFractionRing Nat.instCommSemiring NNRat instCommSemiringNNRat Semiring.toNatAlgebra CommSemiring.toSemiring	—	eq_natCast RingHom.instRingHomClass instCharZero Nat.instNontrivial IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd mul_den_eq_num one_mul

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFractionRing 📖	mathematical	—	IsFractionRing Int.instCommSemiring commSemiring Ring.toIntAlgebra DivisionRing.toRing instDivisionRing	—	eq_intCast RingHom.instRingHomClass instCharZero mem_nonZeroDivisors_iff_ne_zero IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.instNontrivial mul_den_eq_num

(root)

Definitions

Name	Category	Theorems
FractionRing 📖	CompOp	112 math math: RatFunc.mk_def_of_ne, RatFunc.ofFractionRing_mk', RatFunc.mk_coe_def, RatFunc.toFractionRing_injective, ClassGroup.mk0_integralRep, FractionalIdeal.isPrincipal_of_isPrincipal_num, ClassGroup.mk_eq_mk_of_coe_ideal, FractionRing.instIsScalarTower, ClassGroup.Quot_mk_eq_mk, IsDedekindRing.toIsIntegralClosure, RatFunc.smul_def, WittVector.IsocrystalHom.frob_equivariant, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Cardinal.mk_fractionRing, instIsScalarTowerAtPrimeFractionRing_1, instIsFractionRingAtPrimeFractionRing, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, FractionalIdeal.isUnit_num, FractionRing.algebraMap_liftAlgebra, FractionRing.isSeparable_of_isLocalization, instIsPushoutFractionRingPolynomial_1, coeSubmodule_differentIdeal_fractionRing, RatFunc.mk_def, RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Algebra.algebraMap_intNorm_fractionRing, RatFunc.toFractionRing_smul, FractionRing.instIsScalarTower_1, Module.Finite.instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, IsFractionRing.instAtPrimeFractionRing, RatFunc.ofFractionRing_one, FractionRing.cardinalMk, RatFunc.ofFractionRing_zero, AlgebraicIndependent.lift_reprField, RatFunc.ofFractionRing_add, WittVector.IsocrystalEquiv.frob_equivariant, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsScalarTowerAtPrimeFractionRing, RatFunc.ofFractionRing_comp_algebraMap, map_equiv_traceDual, FractionRing.instIsFractionRing, Ideal.relNorm_algebraMap', Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, RatFunc.liftRingHom_ofFractionRing_algebraMap, RatFunc.one_def, RatFunc.inv_def, Ideal.relNorm_algebraMap, WittVector.inv_pair₂, WittVector.exists_frobenius_solution_fractionRing, IsGaloisGroup.toFractionRing, RatFunc.ofFractionRing_smul, WittVector.inv_pair₁, RatFunc.zero_def, RatFunc.ofFractionRing_injective, RatFunc.ofFractionRing_sub, AlgebraicIndependent.liftAlgHom_comp_reprField, RatFunc.ofFractionRing_neg, ClassGroup.mk_eq_mk, ClassGroup.equivPic_symm_apply, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, WittVector.StandardOneDimIsocrystal.frobenius_apply, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, IsLocalization.instIsScalarTowerAtPrimeFractionRing, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, RatFunc.mk_def_of_mem, AlgebraicIndependent.aevalEquivField_apply_coe, IsFractionRing.charP, Algebra.IsAlgebraic.rank_fractionRing, instIsPushoutFractionRingPolynomial, RatFunc.ofFractionRing_inv, Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, RatFunc.neg_def, RatFunc.ofFractionRing_eq, RatFunc.mk_zero, WittVector.exists_frobenius_solution_fractionRing_aux, ClassGroup.mk_eq_one_of_coe_ideal, RatFunc.mk_one', FractionRing.isScalarTower_liftAlgebra, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, RatFunc.sub_def, RatFunc.div_def, RatFunc.add_def, Algebra.algebraMap_intTrace_fractionRing, RatFunc.toFractionRingRingEquiv_symm_eq, MvRatFunc.rank_eq_max_lift, ClassGroup.equivPic_apply, RatFunc.toFractionRingRingEquiv_apply, Ideal.absNorm_algebraMap, Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, FractionRing.instFaithfulSMul, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, RatFunc.mul_def, Ring.instIsGaloisFractionRingNormalClosure, ClassGroup.integralRep_mem_nonZeroDivisors, instFiniteDimensionalFractionRingOfFinite, RatFunc.toFractionRingAlgEquiv_apply, FractionRing.instNontrivial, Algebra.IsAlgebraic.rank_fractionRing_polynomial, ClassGroup.mk_def, FractionRing.mk_eq_div, instIsPushoutFractionRingMvPolynomial_1, RatFunc.ofFractionRing_algebraMap, IsFractionRing.charZero, instIsPushoutFractionRingMvPolynomial, RatFunc.ofFractionRing_mul, RatFunc.toFractionRing_eq
IsFractionRing 📖	MathDef	45 math math: AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, IsIntegralClosure.isFractionRing_of_finite_extension, Localization.isFractionRing_range_mapToFractionRing, AlgebraicGeometry.ValuativeCommSq.isFractionRing, instIsFractionRing, NumberField.RingOfIntegers.instIsFractionRing, AlgebraicGeometry.functionField_isFractionRing_of_affine, instIsFractionRingAtPrimeFractionRing, CyclotomicRing.instIsFractionRingCyclotomicFieldOfIsDomainOfNeZeroCast, IsFractionRing.of_ringEquiv_left, IsFractionRing.self_iff_surjective, IsFractionRing.isFractionRing_of_isLocalization, RatFunc.instIsFractionRingPolynomial, IsFractionRing.instAtPrimeFractionRing, integralClosure.isFractionRing_of_finite_extension, IsFractionRing.isFractionRing_iff_of_base_ringEquiv, NNRat.isFractionRing, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, IsFractionRing.idem, Valuation.Integers.isFractionRing, IsFractionRing.of_field, ValuationRing.isFractionRing_iff, FractionRing.instIsFractionRing, PadicInt.isFractionRing, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, ValuationSubring.instIsFractionRingSubtypeMem, Rat.isFractionRing, integralClosure.isFractionRing_of_algebraic, IsFractionRing.isFractionRing_of_isDomain_of_isLocalization, WithVal.instIsFractionRing, Localization.subalgebra.isFractionRing, IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, IsIntegralClosure.isFractionRing_of_algebraic, Localization.subalgebra.isFractionRing_ofField, FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, IsFractionRing.trans, IsFractionRing.self_iff_nonZeroDivisors_le_isUnit, LaurentSeries.instIsFractionRingPowerSeries, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit, isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective, ValuationRing.instIsFractionRingInteger, instIsFractionRingQuotientIdealResidueField, IsFractionRing.self_iff_bijective, Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_injective_of_field_isFractionRing 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	Function.Injective.of_comp RingHom.coe_comp IsScalarTower.algebraMap_eq RingHom.injective DivisionRing.isSimpleRing IsFractionRing.injective
instIsFractionRing 📖	mathematical	—	IsFractionRing Semifield.toCommSemiring Field.toSemifield Algebra.id	—	IsLocalization.at_units isUnit_of_mem_nonZeroDivisors
instIsLocalizationIntPosRat 📖	mathematical	—	IsLocalization Int.instCommSemiring Submonoid.pos NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Int.instZeroLEOneClass Rat.commSemiring Ring.toIntAlgebra DivisionRing.toRing Rat.instDivisionRing	—	IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Int.instZeroLEOneClass eq_intCast RingHom.instRingHomClass Rat.instCharZero LT.lt.ne' Subtype.prop IsLocalization.surj Rat.isFractionRing lt_or_gt_of_ne Int.instNontrivial Int.cast_neg mul_neg one_mul

---

← Back to Index