Lemmas

📁 Source: Mathlib/Data/Rat/Cast/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems coe_ofScientific, cast_mk, cast_pow, cast_zpow_of_ne_zero, cast_inv_int, cast_inv_nat, cast_nnratCast, cast_ofScientific, cast_pow	9
Total	9

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_mk 📖	mathematical	—	cast DivisionRing.toNNRatCast DivisionRing.toRatCast	—	cast_def Nat.cast_natAbs Rat.cast_def abs_of_nonneg Int.instAddLeftMono
cast_pow 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield	—	cast_def den_pow num_pow Nat.cast_pow div_eq_mul_inv inv_pow Commute.mul_pow Nat.cast_commute
cast_zpow_of_ne_zero 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat instZPow DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	zpow_natCast cast_pow zpow_neg cast_inv_of_ne_zero

NNRat.Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofScientific 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NNRatCast.toOfScientific Nonneg.instNNRatCast Field.toSemifield DivisionRing.toNNRatCast Field.toDivisionRing	—	—

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_inv_int 📖	mathematical	—	DivisionRing.toRatCast InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	Int.cast_natCast cast_inv_nat Int.cast_negSucc inv_neg cast_neg
cast_inv_nat 📖	mathematical	—	DivisionRing.toRatCast InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing	—	Nat.cast_zero inv_zero cast_zero cast_def inv_natCast_num inv_natCast_den Int.cast_one one_div
cast_nnratCast 📖	mathematical	—	DivisionRing.toRatCast NNRat.cast instNNRatCast DivisionRing.toNNRatCast	—	cast_def NNRat.cast_def num_div_eq_of_coprime NNRat.den_pos NNRat.coprime_num_den den_div_eq_of_coprime Int.cast_natCast Int.instCharZero
cast_ofScientific 📖	mathematical	—	DivisionRing.toRatCast NNRatCast.toOfScientific DivisionRing.toNNRatCast	—	NNRat.cast_ofScientific cast_nnratCast
cast_pow 📖	mathematical	—	DivisionRing.toRatCast Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	cast_def Nat.cast_pow Int.cast_pow div_eq_mul_inv inv_pow Commute.mul_pow Int.cast_commute

---

← Back to Index