Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/CharP/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `cast_ne_zero_of_ne_of_prime`, `charP_iff_prime_eq_zero`, `intCast_eq_intCast`, `intCast_eq_intCast_mod`, `intCast_injOn_Ico`, `natCast_eq_natCast`, `natCast_eq_natCast'`, `natCast_eq_natCast_mod`, `natCast_injOn_Iio`, `ringChar_of_prime_eq_zero`, `charZero_iff_forall_prime_ne_zero`, `charP`, `cast_injOn_of_ringChar_ne_two`, `charP`, `charP`, `charP`, `charZero_of_left`, `charZero_of_right`, `eq_self_iff_eq_zero_of_char_ne_two`, `neg_one_ne_one_of_char_ne_two`, `two_ne_zero`, `charP`, `instExpCharProd`, `instIsCharPOfIsLeftCancelAddOfCharP`	24
Total	24

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_ne_zero_of_ne_of_prime` 📖	—	`Nat.Prime`	—	—	`Nat.Prime.eq_one_or_self_of_dvd` `cast_eq_zero_iff` `false_of_nontrivial_of_char_one`
`charP_iff_prime_eq_zero` 📖	mathematical	`Nat.Prime`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`cast_eq_zero` `ringChar.charP` `ringChar_of_prime_eq_zero`
`intCast_eq_intCast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Int.ModEq`	—	`sub_eq_zero` `Int.cast_sub` `intCast_eq_zero_iff` `Int.modEq_iff_dvd`
`intCast_eq_intCast_mod` 📖	mathematical	—	`AddGroupWithOne.toIntCast`	—	`intCast_eq_intCast` `Int.ModEq.symm` `Int.mod_modEq`
`intCast_injOn_Ico` 📖	mathematical	—	`Set.InjOn` `AddGroupWithOne.toIntCast` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `natCast_injOn_Iio` `Int.cast_natCast`
`natCast_eq_natCast` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `Nat.ModEq`	—	`Nat.modEq_iff_dvd'` `cast_eq_zero_iff` `add_right_cancel_iff` `zero_add` `Nat.cast_add` `le_of_not_ge` `Nat.ModEq.comm`
`natCast_eq_natCast'` 📖	mathematical	`Nat.ModEq`	`AddMonoidWithOne.toNatCast`	—	`Nat.cast_add` `cast_eq_zero_iff` `Nat.modEq_iff_dvd'` `zero_add` `Nat.ModEq.symm` `le_of_not_ge`
`natCast_eq_natCast_mod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`natCast_eq_natCast'` `Nat.ModEq.symm` `Nat.mod_modEq`
`natCast_injOn_Iio` 📖	mathematical	—	`Set.InjOn` `AddMonoidWithOne.toNatCast` `Set.Iio` `Nat.instPreorder`	—	`Nat.ModEq.eq_of_lt_of_lt` `natCast_eq_natCast`
`ringChar_of_prime_eq_zero` 📖	mathematical	`Nat.Prime` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`ringChar`	—	`Nat.dvd_prime` `ringChar.dvd` `ringChar_ne_one`

CharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charZero_iff_forall_prime_ne_zero` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`Nat.Prime.ne_zero` `CharP.char_is_prime_or_zero` `ringChar.charP` `CharP.cast_eq_zero` `CharP.charP_to_charZero`

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `instAddMonoidWithOne`	—	`natCast_eq_zero`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_injOn_of_ringChar_ne_two` 📖	mathematical	—	`Set.InjOn` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`cast_zero` `cast_one` `NeZero.one` `cast_neg` `Ring.neg_one_ne_one_of_char_ne_two`

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `MulOpposite` `instAddMonoidWithOne`	—	`CharP.cast_eq_zero_iff`

Nat.lcm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `Prod.instAddMonoidWithOne`	—	`Prod.fst_natCast` `CharP.cast_eq_zero_iff` `Prod.snd_natCast`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `instAddMonoidWithOne`	—	`Nat.lcm.charP`
`charZero_of_left` 📖	mathematical	—	`CharZero` `instAddMonoidWithOne`	—	`CharZero.cast_injective`
`charZero_of_right` 📖	mathematical	—	`CharZero` `instAddMonoidWithOne`	—	`CharZero.cast_injective`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_self_iff_eq_zero_of_char_ne_two` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_eq_zero` `two_mul` `neg_eq_iff_add_eq_zero` `two_ne_zero` `neg_zero`
`neg_one_ne_one_of_char_ne_two` 📖	—	—	—	—	`two_ne_zero` `neg_eq_iff_add_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two`
`two_ne_zero` 📖	—	—	—	—	`Nat.instAtLeastTwoHAddOfNat` `ringChar.spec` `Nat.dvd_prime` `Nat.prime_two` `CharP.ringChar_ne_one`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `addMonoidWithOne`	—	`ext_iff` `CharP.cast_eq_zero_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instExpCharProd` 📖	mathematical	—	`ExpChar` `Prod.instAddMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Prod.charZero_of_left` `Nat.not_prime_one` `Prod.charP`
`instIsCharPOfIsLeftCancelAddOfCharP` 📖	mathematical	—	`Semiring.toGrindSemiring`	—	`CharP.cast_eq_iff_mod_eq`

---

← Back to Index