Documentation Verification Report

Algebra

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

Statistics

Metric	Count
Definitions	0
Theorems `charP_iff`, `ringChar_eq`, `dvd_of_ringHom`, `of_ringHom_of_ne_zero`, `of_injective_algebraMap'`, `charP`, `charZero`, `charP`, `charP_of_isFractionRing`, `charZero`, `charZero_of_isFractionRing`, `charP`, `charP_iff`, `charP_iff_charP`, `expChar`, `expChar_iff`, `charP`, `expChar`, `charP_zero`, `charZero`, `charP_of_injective_algebraMap`, `charP_of_injective_algebraMap'`, `charP_of_injective_ringHom`, `charZero_of_injective_algebraMap`, `charZero_of_injective_ringHom`, `expChar_of_injective_algebraMap`, `expChar_of_injective_ringHom`	27
Total	27

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_iff` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHom.charP_iff_charP`
`ringChar_eq` 📖	mathematical	—	`ringChar` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring`	—	`ringChar.eq_iff` `charP_iff` `ringChar.charP`

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_ringHom` 📖	—	—	—	—	`cast_eq_zero_iff` `map_natCast` `RingHom.instRingHomClass` `cast_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`of_ringHom_of_ne_zero` 📖	mathematical	—	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHom.domain_nontrivial` `char_is_prime_or_zero` `exists` `dvd_of_ringHom` `Nat.isUnit_iff` `Irreducible.isUnit_or_isUnit` `Iff.not` `char_ne_one` `mul_one`

ExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective_algebraMap'` 📖	mathematical	—	`ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`expChar_of_injective_ringHom` `FaithfulSMul.algebraMap_injective`

FreeAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `FreeAlgebra` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiring`	—	`charP_of_injective_algebraMap` `algebraMap_leftInverse`
`charZero` 📖	mathematical	—	`CharZero` `FreeAlgebra` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiring`	—	`charZero_of_injective_algebraMap` `algebraMap_leftInverse`

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `FractionRing` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OreLocalization.instRing` `CommRing.toRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid`	—	`charP_of_isFractionRing` `Localization.isLocalization`
`charP_of_isFractionRing` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`charP_of_injective_algebraMap` `injective`
`charZero` 📖	mathematical	—	`CharZero` `FractionRing` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OreLocalization.instRing` `CommRing.toRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid`	—	`charZero_of_isFractionRing` `Localization.isLocalization`
`charZero_of_isFractionRing` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`CharP.charP_to_charZero` `charP_of_isFractionRing` `CharP.ofCharZero`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`CharP.exists` `CharP.eq` `charP_of_injective_ringHom`
`charP_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`charP_of_injective_ringHom` `charP`
`charP_iff_charP` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`injective` `DivisionRing.isSimpleRing` `map_natCast` `instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`expChar` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`ExpChar` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`charZero` `charP`
`expChar_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`ExpChar` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`expChar_of_injective_ringHom` `expChar`

Subfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `Subfield` `SetLike.instMembership` `instSetLike` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingSubtypeMem`	—	`RingHom.charP` `subtype_injective`
`expChar` 📖	mathematical	—	`ExpChar` `Subfield` `SetLike.instMembership` `instSetLike` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingSubtypeMem`	—	`RingHom.expChar` `subtype_injective`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_of_injective_algebraMap` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`charP_of_injective_ringHom`
`charP_of_injective_algebraMap'` 📖	mathematical	—	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`charP_of_injective_ringHom` `FaithfulSMul.algebraMap_injective`
`charP_of_injective_ringHom` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`CharP.cast_eq_zero_iff` `map_natCast` `RingHom.instRingHomClass` `map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`charZero_of_injective_algebraMap` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`CharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`charZero_of_injective_ringHom`
`charZero_of_injective_ringHom` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`CharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`CharZero.cast_injective` `map_natCast` `RingHom.instRingHomClass`
`expChar_of_injective_algebraMap` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`ExpChar` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`expChar_of_injective_ringHom`
`expChar_of_injective_ringHom` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`ExpChar` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`charZero_of_injective_ringHom` `charP_of_injective_ringHom`

algebraRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_zero` 📖	mathematical	—	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`charP_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `CharP.ofCharZero` `Rat.instCharZero`
`charZero` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`CharP.charP_to_charZero` `charP_zero`

---

← Back to Index