NumDen

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

Statistics

Metric	Count
Definitions den, num	2
Theorems associated_den_num_inv, associated_num_den_inv, eq_zero_of_num_eq_zero, exists_reduced_fraction, isInteger_of_isUnit_den, isUnit_den_iff, isUnit_den_zero, mk'_num_den, mk'_num_den', num_den_reduced, num_den_unique, num_eq_zero, num_mul_den_eq_num_iff_eq, num_mul_den_eq_num_iff_eq', num_mul_den_eq_num_mul_den_iff_eq, num_zero	16
Total	18

IsFractionRing

Definitions

Name	Category	Theorems
den 📖	CompOp	15 math math: Rat.isFractionRingDen, num_isRoot_scaleRoots_of_aeval_eq_zero, Rat.associated_num_den, mk'_num_den', mk'_num_den, den_dvd_of_is_root, associated_num_den_inv, num_mul_den_eq_num_mul_den_iff_eq, num_mul_den_eq_num_iff_eq, num_den_unique, num_den_reduced, associated_den_num_inv, num_mul_den_eq_num_iff_eq', isUnit_den_zero, isUnit_den_iff
num 📖	CompOp	15 math math: num_isRoot_scaleRoots_of_aeval_eq_zero, Rat.associated_num_den, num_eq_zero, mk'_num_den', mk'_num_den, associated_num_den_inv, num_dvd_of_is_root, Rat.isFractionRingNum, num_mul_den_eq_num_mul_den_iff_eq, num_zero, num_mul_den_eq_num_iff_eq, num_den_unique, num_den_reduced, associated_den_num_inv, num_mul_den_eq_num_iff_eq'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_den_num_inv 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den num InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	associated_of_dvd_dvd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero IsRelPrime.dvd_of_dvd_mul_right instDecompositionMonoidOfNonemptyGCDMonoid instNonemptyGCDMonoidOfNormalizedGCDMonoid instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid IsRelPrime.symm num_den_reduced dvd_of_mul_left_dvd dvd_of_eq FaithfulSMul.algebraMap_injective instFaithfulSMul eq_of_div_eq_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_div_mul_comm mk'_num_den' inv_mul_cancel₀ mul_inv_cancel₀
associated_num_den_inv 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring num Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	Associated.symm associated_den_num_inv inv_ne_zero inv_inv
eq_zero_of_num_eq_zero 📖	mathematical	num MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Field.toCommRing	—	num_mul_den_eq_num_iff_eq' MulZeroClass.zero_mul map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
exists_reduced_fraction 📖	mathematical	—	IsRelPrime MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors IsLocalization.mk' Semifield.toCommSemiring Field.toSemifield	—	IsLocalization.exists_integer_multiple UniqueFactorizationMonoid.exists_reduced_factors' mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial mul_mem_nonZeroDivisors mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain to_map_ne_zero_of_mem_nonZeroDivisors map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Algebra.smul_def mul_assoc IsLocalization.mk'_spec'
isInteger_of_isUnit_den 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den	IsLocalization.IsInteger Semifield.toCommSemiring Field.toSemifield	—	to_map_ne_zero_of_mem_nonZeroDivisors IsDomain.toNontrivial trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_units_inv MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain mul_assoc mul_inv_cancel₀ one_mul IsLocalization.mk'_spec' mk'_num_den
isUnit_den_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den IsLocalization.IsInteger Semifield.toCommSemiring Field.toSemifield	—	isInteger_of_isUnit_den IsRelPrime.isUnit_of_dvd IsRelPrime.symm num_den_reduced FaithfulSMul.algebraMap_injective instFaithfulSMul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_comm div_eq_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass nonZeroDivisors.coe_ne_zero IsDomain.toNontrivial mk'_num_den'
isUnit_den_zero 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	—
mk'_num_den 📖	mathematical	—	IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield num den	—	exists_reduced_fraction
mk'_num_den' 📖	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 num Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den	—	mk'_eq_div mk'_num_den
num_den_reduced 📖	mathematical	—	IsRelPrime MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring num Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den	—	exists_reduced_fraction
num_den_unique 📖	mathematical	IsRelPrime MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors IsLocalization.mk' Semifield.toCommSemiring Field.toSemifield	Associated num den	—	associated_of_dvd_dvd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero IsRelPrime.dvd_of_dvd_mul_right instDecompositionMonoidOfNonemptyGCDMonoid instNonemptyGCDMonoidOfNormalizedGCDMonoid instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid num_den_reduced dvd_mul_right FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsSimpleRing.instNontrivial DivisionRing.isSimpleRing FaithfulSMul.to_isTorsionFree instFaithfulSMul IsDomain.toNontrivial instIsDomain IsLocalization.mk'_eq_iff_eq' mk'_num_den IsRelPrime.dvd_of_dvd_mul_left IsRelPrime.symm dvd_mul_left
num_eq_zero 📖	mathematical	—	num MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	eq_zero_of_num_eq_zero num_zero
num_mul_den_eq_num_iff_eq 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den num	—	mk'_num_den IsLocalization.eq_mk'_iff_mul_eq
num_mul_den_eq_num_iff_eq' 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den num	—	mk'_num_den IsLocalization.eq_mk'_iff_mul_eq
num_mul_den_eq_num_mul_den_iff_eq 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing num Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors den	—	mk'_num_den IsLocalization.mk'_eq_of_eq'
num_zero 📖	mathematical	—	num MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	mk'_num_den' instFaithfulSMul IsDomain.toNontrivial

---

← Back to Index