FractionRing

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

Statistics

Metric	Count
Definitions FractionRing, algEquiv, liftAlgebra, unique, IsFractionRing, algEquiv, algEquivOfAlgEquiv, fieldEquivOfAlgEquiv, fieldEquivOfAlgEquivHom, inv, liftAlgHom, map, ringEquivOfRingEquiv, toField	14
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, 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	65
Total	79

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
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	liftAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike lift AlgHom.toRingHom	—	—
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 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	liftAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike lift AlgHom.toRingHom	—	—
liftAlgHom_toRingHom 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	AlgHom.toRingHom liftAlgHom lift	—	—
lift_algebraMap 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	lift 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 DivisionRing.toRing Subring.instSetLike RingHom.range CommRing.toRing	—	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 CommRing.toRing DivisionRing.toRing Field.toDivisionRing Subring.closure	RingHom.fieldRange 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	lift IsLocalization.mk' nonZeroDivisors Semiring.toMonoidWithZero 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' Semifield.toCommSemiring Field.toSemifield NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring 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 Semifield.toCommSemiring	—	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
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 DivisionRing.toRing Subring.instSetLike RingHom.range CommRing.toRing	—	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 CommRing.toRing DivisionRing.toRing Field.toDivisionRing Subring.closure	RingHom.fieldRange 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	110 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, 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, 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, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, 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, 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	44 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.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