Lemmas

📁 Source: Mathlib/Data/NNRat/Lemmas.lean

Statistics

Metric	Count
Definitions rec	1
Theorems coe_indicator, den_mul_den_eq_den_mul_gcd, mul_den, mul_num, num_mul_num_eq_num_mul_gcd, toNNRat_div, toNNRat_div', toNNRat_inv	8
Total	9

NNRat

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_indicator 📖	mathematical	—	cast Rat.instNNRatCast Set.indicator NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing	—	map_indicator MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
den_mul_den_eq_den_mul_gcd 📖	mathematical	—	den NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield num	—	num_coe Rat.den_mul_den_eq_den_mul_gcd
mul_den 📖	mathematical	—	den NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield num	—	num_coe Rat.mul_den
mul_num 📖	mathematical	—	num NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield den	—	Nat.cast_mul num_coe Int.instCharZero Rat.mul_num
num_mul_num_eq_num_mul_gcd 📖	mathematical	—	num NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield den	—	Nat.cast_mul num_coe Int.instCharZero Rat.num_mul_num_eq_num_mul_gcd

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNNRat_div 📖	mathematical	—	toNNRat NNRat NNRat.instDiv	—	div_eq_mul_inv toNNRat_inv toNNRat_mul
toNNRat_div' 📖	mathematical	—	toNNRat NNRat NNRat.instDiv	—	div_eq_inv_mul toNNRat_mul inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing toNNRat_inv
toNNRat_inv 📖	mathematical	—	toNNRat NNRat NNRat.instInv	—	le_total toNNRat_eq_zero inv_zero inv_nonpos instPosMulMono coe_toNNRat NNRat.coe_inv NNRat.toNNRat_coe

---

← Back to Index