Documentation Verification Report

Basic

📁 Source: Mathlib/Data/Nat/Cast/Basic.lean

Statistics

Metric	Count
Definitions `castAddMonoidHom`, `castRingHom`, `uniqueRingHom`, `instNatCast`, `instOfNat`	5
Theorems `natCast`, `natCast`, `ext_nat`, `ext_nat_iff`, `castRingHom_nat`, `cast_dvd_cast`, `cast_id`, `cast_mul`, `cast_pow`, `coe_castAddMonoidHom`, `coe_castRingHom`, `ofNat_nsmul_eq_mul`, `nat_of_neZero`, `natCast_apply`, `natCast_def`, `ofNat_apply`, `ofNat_def`, `eq_natCast'`, `elim_natCast_natCast`, `eq_natCast`, `eq_natCast'`, `ext_nat`, `ext_nat''`, `map_natCast`, `map_natCast'`, `map_ofNat`, `map_ofNat'`, `nsmul_eq_mul'`	28
Total	33

Dvd.dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natCast` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Nat.cast_dvd_cast`

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natCast` 📖	mathematical	`Even`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`map` `AddMonoidHom.instAddMonoidHomClass`

MonoidWithZeroHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_nat` 📖	—	`DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `funLike`	—	—	`ext_nat''` `MonoidWithZeroHomClass.toZeroHomClass` `monoidWithZeroHomClass`
`ext_nat_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `funLike`	—	`ext_nat`

Nat

Definitions

Name	Category	Theorems
`castAddMonoidHom` 📖	CompOp	2 math math: `coe_castAddMonoidHom`, `AddSubmonoid.one_eq_mrange`
`castRingHom` 📖	CompOp	6 math math: `castRingHom_nat`, `RingHom.eq_natCast'`, `coe_castRingHom`, `Ideal.map_comap_natCastRingHom_int`, `CharP.quotient_iff_le_ker_natCast`, `MonoidWithZeroHomClass.ext_nnrat_iff`
`uniqueRingHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castRingHom_nat` 📖	mathematical	—	`castRingHom` `instNonAssocSemiring` `RingHom.id`	—	—
`cast_dvd_cast` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`cast_id` 📖	—	—	—	—	—
`cast_mul` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`MulZeroClass.mul_zero` `cast_zero` `mul_add` `Distrib.leftDistribClass` `mul_one` `cast_add` `cast_one`
`cast_pow` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_zero` `cast_one` `pow_succ'` `cast_mul`
`coe_castAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddMonoidHom.instFunLike` `castAddMonoidHom` `AddMonoidWithOne.toNatCast`	—	—
`coe_castRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `instNonAssocSemiring` `RingHom.instFunLike` `castRingHom` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`ofNat_nsmul_eq_mul` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`nsmul_eq_mul`

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nat_of_neZero` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`of_map` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_natCast`

Pi

Definitions

Name	Category	Theorems
`instNatCast` 📖	CompOp	41 math math: `differentiableAt_natCast`, `derivWithin_natCast`, `Matrix.diagonal_natCast'`, `differentiableWithinAt_natCast`, `hasStrictFDerivAt_natCast`, `MeromorphicOn.divisor_natCast`, `hasDerivAtFilter_natCast`, `MeasureTheory.lpNorm_mul_natCast`, `ModularForm.coe_natCast`, `BoundedContinuousFunction.coe_natCast`, `meromorphicOrderAt_const_natCast`, `MeasureTheory.uniformIntegrable_average_real`, `differentiable_natCast`, `EisensteinSeries.finGcdMap_div`, `natCast_apply`, `SlashInvariantForm.coe_natCast`, `hasDerivWithinAt_natCast`, `fderiv_natCast`, `Finsupp.card_pi`, `fwdDiff_iter_eq_factorial`, `DFinsupp.card_pi`, `hasFDerivWithinAt_natCast`, `fderivWithin_natCast`, `hasDerivAt_natCast`, `deriv_natCast`, `MeasureTheory.lpNorm_div_natCast`, `lp.infty_coeFn_natCast`, `hasFDerivAt_natCast`, `ContinuousMap.coe_natCast`, `Sum.elim_natCast_natCast`, `Polynomial.fwdDiff_iter_degree_eq_factorial`, `measurable_natCast`, `hasStrictDerivAt_natCast`, `MeasureTheory.lpNorm_natCast_mul`, `Function.mulSupport_natCast`, `hasFDerivAtFilter_natCast`, `differentiableOn_natCast`, `natCast_def`, `Module.rankAtStalk_eq_finrank_of_free`, `Function.support_natCast`, `natCast_memℓp_infty`
`instOfNat` 📖	CompOp	2 math math: `ofNat_def`, `CartanMatrix.A_diag`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natCast_apply` 📖	mathematical	—	`instNatCast`	—	—
`natCast_def` 📖	mathematical	—	`instNatCast`	—	—
`ofNat_apply` 📖	—	—	—	—	—
`ofNat_def` 📖	mathematical	—	`instOfNat`	—	—

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_natCast'` 📖	mathematical	—	`Nat.castRingHom`	—	`ext` `eq_natCast` `instRingHomClass`

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim_natCast_natCast` 📖	mathematical	—	`Pi.instNatCast`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_natCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`eq_natCast'` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`eq_natCast'` 📖	mathematical	`DFunLike.coe` `AddMonoidWithOne.toOne`	`AddMonoidWithOne.toNatCast`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `Nat.cast_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `Nat.cast_add_one`
`ext_nat` 📖	—	—	—	—	`ext_nat'` `RingHomClass.toAddMonoidHomClass` `eq_natCast` `Nat.cast_one`
`ext_nat''` 📖	—	`DFunLike.coe`	—	—	`DFunLike.ext` `map_zero`
`map_natCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`map_natCast'` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_natCast'` 📖	mathematical	`DFunLike.coe` `AddMonoidWithOne.toOne`	`AddMonoidWithOne.toNatCast`	—	`eq_natCast'` `AddMonoidHom.instAddMonoidHomClass` `Nat.cast_one`
`map_ofNat` 📖	mathematical	—	`DFunLike.coe` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`map_natCast`
`map_ofNat'` 📖	mathematical	`DFunLike.coe` `AddMonoidWithOne.toOne`	`instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast`	—	`map_natCast'`
`nsmul_eq_mul'` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast`	—	`zero_nsmul` `Nat.cast_zero` `MulZeroClass.mul_zero` `succ_nsmul` `Nat.cast_succ` `mul_add` `Distrib.leftDistribClass` `mul_one`

---

← Back to Index