Rat

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

Statistics

Metric	Count
Definitions	0
Theorems associated_num_den, isFractionRingDen, isFractionRingNum, isLocalizationIsInteger_iff	4
Total	4

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_num_den 📖	mathematical	—	Associated Int.instMonoid IsFractionRing.num Int.instCommRing Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain Int.euclideanDomain instField Ring.toIntAlgebra DivisionRing.toRing instDivisionRing isFractionRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors IsFractionRing.den	—	IsFractionRing.num_den_unique Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain isFractionRing IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.instNontrivial IsBezout.span_pair_isPrincipal IsBezout.of_isPrincipalIdealRing IsFractionRing.mk'_eq_div eq_intCast RingHom.instRingHomClass map_natCast num_div_den
isFractionRingDen 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing SetLike.instMembership Submonoid.instSetLike nonZeroDivisors IsFractionRing.den Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain Int.euclideanDomain instField Ring.toIntAlgebra DivisionRing.toRing instDivisionRing isFractionRing	—	Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain isFractionRing associated_num_den
isFractionRingNum 📖	mathematical	—	Associated Int.instMonoid IsFractionRing.num Int.instCommRing Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain Int.euclideanDomain instField Ring.toIntAlgebra DivisionRing.toRing instDivisionRing isFractionRing	—	Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain isFractionRing associated_num_den
isLocalizationIsInteger_iff 📖	mathematical	—	IsLocalization.IsInteger Int.instCommSemiring commSemiring Ring.toIntAlgebra DivisionRing.toRing instDivisionRing Set Set.instMembership Set.range	—	eq_intCast RingHom.instRingHomClass

---

← Back to Index