Basic

Statistics

Metric	Count
Definitions	0
Theorems `dvd_natCast`, `eq_of_mod_eq_of_natAbs_sub_lt_natAbs`, `eq_zero_of_dvd_of_nonneg_of_lt`, `gcd_emod`, `inductionOn'_add_one`, `instNontrivial`, `natAbs_le_of_dvd_ne_zero`, `natAbs_surjective`, `natCast_dvd`, `natCast_dvd_ofNat`, `ofNat_dvd_natCast`, `ofNat_injective`, `pow_right_injective`, `strongRec_of_ge`	14
Total	14

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_natCast` 📖	—	—	—	—	—
`eq_of_mod_eq_of_natAbs_sub_lt_natAbs` 📖	—	—	—	—	—
`eq_zero_of_dvd_of_nonneg_of_lt` 📖	—	—	—	—	—
`gcd_emod` 📖	—	—	—	—	—
`inductionOn'_add_one` 📖	mathematical	—	`inductionOn'`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `inductionOn'.eq_1`
`instNontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`natAbs_le_of_dvd_ne_zero` 📖	—	—	—	—	`not_lt`
`natAbs_surjective` 📖	—	—	—	—	—
`natCast_dvd` 📖	—	—	—	—	—
`natCast_dvd_ofNat` 📖	—	—	—	—	—
`ofNat_dvd_natCast` 📖	—	—	—	—	—
`ofNat_injective` 📖	—	—	—	—	—
`pow_right_injective` 📖	—	—	—	—	`Function.Injective.of_comp` `Nat.pow_right_injective`
`strongRec_of_ge` 📖	mathematical	—	`strongRec`	—	`strongRec.eq_1` `inductionOn'_self` `strongRec_of_lt` `inductionOn'_add_one` `inductionOn'_sub_one`

---