Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions	0
Theorems `ext_nnrat`, `ext_nnrat'`, `ext_nnrat_iff`, `ext_nnrat_on_pnat`, `ext_rat`, `ext_rat'`, `ext_rat_iff`, `ext_rat_on_pnat`, `cast_add_of_ne_zero`, `cast_comm`, `cast_commute`, `cast_divNat_of_ne_zero`, `cast_div_of_ne_zero`, `cast_inv_of_ne_zero`, `cast_mul_of_ne_zero`, `cast_natCast`, `cast_ofNat`, `cast_one`, `cast_zero`, `commute_cast`, `subsingleton_ringHom`, `cast_add_of_ne_zero`, `cast_comm`, `cast_commute`, `cast_divInt_of_ne_zero`, `cast_div_of_ne_zero`, `cast_intCast`, `cast_inv_of_ne_zero`, `cast_mkRat_of_ne_zero`, `cast_mul_of_ne_zero`, `cast_natCast`, `cast_neg`, `cast_ofNat`, `cast_one`, `cast_sub_of_ne_zero`, `cast_zero`, `commute_cast`, `subsingleton_ringHom`, `ext_rat`, `eq_nnratCast`, `eq_ratCast`, `map_nnratCast`, `map_ratCast`	43
Total	43

MonoidWithZeroHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_nnrat` 📖	—	`MonoidWithZeroHom.comp` `NNRat` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `MonoidWithZero.toMulZeroOneClass` `toMonoidWithZeroHom` `RingHom` `Nat.instNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Nat.castRingHom`	—	—	`RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_nnrat'` `MonoidWithZeroHom.monoidWithZeroHomClass` `DFunLike.congr_fun`
`ext_nnrat'` 📖	—	`DFunLike.coe` `NNRat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield`	—	—	`DFunLike.ext` `NNRat.num_div_den` `div_eq_mul_inv` `map_mul` `MonoidHomClass.toMulHomClass` `toMonoidHomClass` `eq_on_inv₀`
`ext_nnrat_iff` 📖	mathematical	—	`MonoidWithZeroHom.comp` `NNRat` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `MonoidWithZero.toMulZeroOneClass` `toMonoidWithZeroHom` `RingHom` `Nat.instNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Nat.castRingHom`	—	`RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_nnrat`
`ext_nnrat_on_pnat` 📖	—	`DFunLike.coe` `NNRat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield`	—	—	`ext_nnrat'` `DFunLike.congr_fun` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_nat''` `toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`ext_rat` 📖	—	`MonoidWithZeroHom.comp` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Rat.semiring` `MonoidWithZero.toMulZeroOneClass` `toMonoidWithZeroHom` `RingHom` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `RingHom.instFunLike` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Int.castRingHom`	—	—	`RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_rat'` `MonoidWithZeroHom.monoidWithZeroHomClass` `DFunLike.congr_fun`
`ext_rat'` 📖	—	`DFunLike.coe`	—	—	`DFunLike.ext` `Rat.num_div_den` `div_eq_mul_inv` `map_mul` `MonoidHomClass.toMulHomClass` `toMonoidHomClass` `Int.cast_natCast` `eq_on_inv₀`
`ext_rat_iff` 📖	mathematical	—	`MonoidWithZeroHom.comp` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `Rat.semiring` `MonoidWithZero.toMulZeroOneClass` `toMonoidWithZeroHom` `RingHom` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `RingHom.instFunLike` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Int.castRingHom`	—	`RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_rat`
`ext_rat_on_pnat` 📖	—	`DFunLike.coe`	—	—	`ext_rat'` `DFunLike.congr_fun` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ext_int'` `MonoidWithZeroHom.monoidWithZeroHomClass` `Int.cast_neg` `Int.cast_one` `Int.cast_natCast`

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_add_of_ne_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`add_def` `cast_divNat_of_ne_zero` `Nat.cast_mul` `mul_ne_zero` `GroupWithZero.noZeroDivisors` `cast_def` `mul_comm` `Commute.div_add_div` `Nat.commute_cast` `Nat.cast_add`
`cast_comm` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `cast` `DivisionSemiring.toNNRatCast`	—	`cast_commute`
`cast_commute` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `cast` `DivisionSemiring.toNNRatCast`	—	`cast_def` `Commute.div_left` `Nat.cast_commute`
`cast_divNat_of_ne_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `divNat` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `Rat.den_dvd` `Nat.cast_mul` `MulZeroClass.zero_mul` `Nat.cast_zero` `cast_def` `Commute.div_eq_div_iff` `Nat.commute_cast`
`cast_div_of_ne_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_def` `cast_divNat_of_ne_zero` `Nat.cast_mul` `mul_ne_zero` `GroupWithZero.noZeroDivisors` `cast_def` `div_eq_mul_inv` `inv_div` `Commute.div_mul_div_comm` `Nat.commute_cast`
`cast_inv_of_ne_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero`	—	`inv_def` `cast_divNat_of_ne_zero` `cast_def` `inv_div`
`cast_mul_of_ne_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`mul_def` `cast_divNat_of_ne_zero` `Nat.cast_mul` `mul_ne_zero` `GroupWithZero.noZeroDivisors` `cast_def` `Commute.div_mul_div_comm` `Nat.commute_cast`
`cast_natCast` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`cast_def` `Nat.cast_one` `div_one`
`cast_ofNat` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast`	—	`cast_natCast`
`cast_one` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`cast_natCast` `Nat.cast_one`
`cast_zero` 📖	mathematical	—	`cast` `DivisionSemiring.toNNRatCast` `NNRat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`cast_natCast` `Nat.cast_zero`
`commute_cast` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `cast` `DivisionSemiring.toNNRatCast`	—	`Commute.symm` `cast_commute`
`subsingleton_ringHom` 📖	mathematical	—	`RingHom` `NNRat` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield`	—	`MonoidWithZeroHomClass.ext_nnrat'` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast`

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_add_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`cast_mkRat_of_ne_zero` `Nat.cast_mul` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `DivisionRing.isDomain` `cast_def` `mul_comm` `Commute.div_add_div` `Nat.cast_commute` `Nat.commute_cast` `Int.cast_add` `Int.cast_mul` `Int.cast_natCast`
`cast_comm` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `DivisionRing.toRatCast`	—	`Commute.eq` `cast_commute`
`cast_commute` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `DivisionRing.toRatCast`	—	`cast_def` `Commute.div_left` `Int.cast_commute` `Nat.cast_commute`
`cast_divInt_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`Int.cast_zero` `den_dvd` `Int.cast_mul` `Int.cast_natCast` `MulZeroClass.zero_mul` `ne_of_gt` `Ne.bot_lt` `cast_def` `div_eq_mul_inv` `eq_div_iff_mul_eq` `mul_assoc` `Commute.eq` `Nat.commute_cast` `mul_inv_cancel₀` `mul_one`
`cast_div_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`div_def'` `cast_divInt_of_ne_zero` `Int.cast_mul` `Int.cast_natCast` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `DivisionRing.isDomain` `cast_def` `div_eq_mul_inv` `inv_div` `Commute.div_mul_div_comm` `Int.commute_cast` `Nat.commute_cast`
`cast_intCast` 📖	mathematical	—	`DivisionRing.toRatCast` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_def` `Nat.cast_one` `div_one`
`cast_inv_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	`cast_divInt_of_ne_zero` `cast_def` `inv_div` `Int.cast_natCast`
`cast_mkRat_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`mkRat_eq_divInt` `cast_divInt_of_ne_zero` `Int.cast_natCast`
`cast_mul_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`mul_eq_mkRat` `cast_mkRat_of_ne_zero` `Nat.cast_mul` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `DivisionRing.isDomain` `cast_def` `Commute.div_mul_div_comm` `Nat.commute_cast` `Int.commute_cast` `Int.cast_mul`
`cast_natCast` 📖	mathematical	—	`DivisionRing.toRatCast` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`Int.cast_natCast` `cast_intCast`
`cast_neg` 📖	mathematical	—	`DivisionRing.toRatCast` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing`	—	`cast_def` `Int.cast_neg` `neg_div`
`cast_ofNat` 📖	mathematical	—	`DivisionRing.toRatCast`	—	`cast_def` `Int.cast_ofNat` `Nat.cast_one` `div_one`
`cast_one` 📖	mathematical	—	`DivisionRing.toRatCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`cast_intCast` `Int.cast_one`
`cast_sub_of_ne_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`sub_eq_add_neg` `cast_add_of_ne_zero` `cast_neg`
`cast_zero` 📖	mathematical	—	`DivisionRing.toRatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`cast_intCast` `Int.cast_zero`
`commute_cast` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `DivisionRing.toRatCast`	—	`Commute.symm` `cast_commute`
`subsingleton_ringHom` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `semiring`	—	`RingHom.ext_rat` `RingHom.instRingHomClass`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_rat` 📖	—	—	—	—	`MonoidWithZeroHomClass.ext_rat'` `RingHomClass.toMonoidWithZeroHomClass` `congr_fun` `ext_int`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_nnratCast` 📖	mathematical	—	`DFunLike.coe` `NNRat` `NNRat.cast` `DivisionSemiring.toNNRatCast`	—	`map_nnratCast` `NNRat.cast_id`
`eq_ratCast` 📖	mathematical	—	`DFunLike.coe` `DivisionRing.toRatCast`	—	`map_ratCast` `Rat.cast_id`
`map_nnratCast` 📖	mathematical	—	`DFunLike.coe` `NNRat.cast` `DivisionSemiring.toNNRatCast`	—	`NNRat.cast_def` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `map_natCast`
`map_ratCast` 📖	mathematical	—	`DFunLike.coe` `DivisionRing.toRatCast`	—	`Rat.cast_def` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `map_intCast` `map_natCast`

---

← Back to Index