Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/CharZero/Defs.lean

Statistics

Metric	Count
Definitions	0
Theorems `cast_injective`, `cast_add_one_ne_zero`, `cast_eq_one`, `cast_eq_zero`, `cast_inj`, `cast_injective`, `cast_ne_one`, `cast_ne_zero`, `charZero`, `charZero_ofNat`, `charZero_one`, `ofNat_eq_ofNat`, `ofNat_ne_one`, `ofNat_ne_zero`, `one_ne_ofNat`, `zero_ne_ofNat`, `charZero_of_inj_zero`	17
Total	17

CharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_injective` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_add_one_ne_zero` 📖	—	—	—	—	`cast_one` `cast_zero`
`cast_eq_one` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddMonoidWithOne.toOne`	—	`cast_one`
`cast_eq_zero` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_zero`
`cast_inj` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`cast_injective`
`cast_injective` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`CharZero.cast_injective`
`cast_ne_one` 📖	—	—	—	—	`Iff.not` `cast_eq_one`
`cast_ne_zero` 📖	—	—	—	—	`cast_eq_zero`

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charZero` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`Nat.cast_ne_zero`
`charZero_ofNat` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast`	—	`OfNat.ofNat_ne_zero`
`charZero_one` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne`	—	`Nat.cast_one` `Nat.cast_ne_zero`

OfNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofNat_eq_ofNat` 📖	—	—	—	—	—
`ofNat_ne_one` 📖	—	—	—	—	`Nat.cast_ne_one` `Nat.AtLeastTwo.ne_one`
`ofNat_ne_zero` 📖	—	—	—	—	`Nat.cast_ne_zero` `Nat.AtLeastTwo.toNeZero`
`one_ne_ofNat` 📖	—	—	—	—	`ofNat_ne_one`
`zero_ne_ofNat` 📖	—	—	—	—	`ofNat_ne_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charZero_of_inj_zero` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne`	—	`Nat.cast_zero` `Nat.cast_succ` `AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index