Documentation Verification Report

CharP

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

Statistics

Metric	Count
Definitions `CharP`, `eqZero`, `fieldOfChar`	3
Theorems `charP_iff_model_fieldOfChar`, `charP_of_model_fieldOfChar`, `model_fieldOfChar_of_charP`, `model_hasChar_of_charP`, `realize_eqZero`	5
Total	8

FirstOrder.Field

Definitions

Name	Category	Theorems
`eqZero` 📖	CompOp	1 math math: `realize_eqZero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_iff_model_fieldOfChar` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ring` `FirstOrder.Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `FirstOrder.Language.Theory.fieldOfChar` `CharP`	—	`instModelField` `Empty.instIsEmpty` `IsDomain.to_noZeroDivisors` `Field.isDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `CharP.ofCharZero` `CharP.charP_to_charZero` `CharP.charP_iff_prime_eq_zero` `CharP.char_is_prime_or_zero`
`charP_of_model_fieldOfChar` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`charP_iff_model_fieldOfChar`
`model_fieldOfChar_of_charP` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ring` `FirstOrder.Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `FirstOrder.Language.Theory.fieldOfChar`	—	`charP_iff_model_fieldOfChar`
`model_hasChar_of_charP` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ring` `FirstOrder.Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `FirstOrder.Language.Theory.fieldOfChar`	—	`FirstOrder.Language.Theory.model_union_iff` `instModelField` `CharP.char_is_prime_or_zero` `IsDomain.to_noZeroDivisors` `Field.isDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Nat.Prime.ne_zero` `Empty.instIsEmpty` `CharP.cast_eq_zero` `CharP.charP_to_charZero`
`realize_eqZero` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `FirstOrder.Language.ring` `FirstOrder.Ring.CompatibleRing.toStructure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `eqZero` `AddMonoidWithOne.toNatCast`	—	`FirstOrder.Ring.realize_termOfFreeCommRing` `map_natCast` `RingHom.instRingHomClass` `FirstOrder.Ring.realize_zero`

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`fieldOfChar` 📖	CompOp	4 math math: `FirstOrder.Field.model_hasChar_of_charP`, `FirstOrder.Field.instModelFieldOfCharOfACF`, `FirstOrder.Field.model_fieldOfChar_of_charP`, `FirstOrder.Field.charP_iff_model_fieldOfChar`

(root)

Definitions

Name	Category	Theorems
`CharP` 📖	CompData	69 math math: `charP_of_card_eq_prime`, `Algebra.charP_iff`, `ringChar.of_eq`, `Nat.lcm.charP`, `algebraRat.charP_zero`, `FirstOrder.Field.charP_of_model_fieldOfChar`, `charP_of_injective_algebraMap`, `charP_of_ne_zero`, `PerfectClosure.instCharP`, `CharP.existsUnique`, `CharP.charP_center_iff`, `CharP.subring'`, `RingHom.charP_iff_charP`, `Fin.charP`, `Polynomial.instCharP`, `CharP.exists'`, `Perfection.charP`, `CharP.exists`, `AlgebraicClosure.instCharP`, `charP_of_injective_ringHom`, `charP_iff`, `IsFractionRing.charP_of_isFractionRing`, `IntermediateField.charP'`, `Polynomial.charP`, `Nimber.instCharPOfNatNat`, `CharP.subring`, `Module.charP_end`, `CharP.addOrderOf_one`, `CharP.congr`, `TruncatedWittVector.charP_zmod`, `MixedCharZero.charP_quotient`, `charP_of_injective_algebraMap'`, `LucasLehmer.X.instCharP`, `CharP.subsemiring`, `CharP.quotient'`, `CharTwo.of_one_ne_zero_of_two_eq_zero`, `IntermediateField.charP`, `ZMod.charP`, `Subfield.charP`, `MvPolynomial.instCharP`, `RingHom.charP`, `MulOpposite.charP`, `RatFunc.instCharP`, `IsFractionRing.charP`, `FreeAlgebra.charP`, `Polynomial.SplittingField.instCharP`, `RingHom.charP_iff`, `CharP.quotient`, `instCharPLinearMapSubtypeMemSubringCenterId`, `CharP.charP_zero_iff_charZero`, `charP_of_prime_pow_injective`, `CharP.pi'`, `CharP.of_ringHom_of_ne_zero`, `charP_of_card_eq_prime_pow`, `FiniteField.card'`, `PreTilt.instCharP`, `CharP.ofCharZero`, `Prod.charP`, `Matrix.charP`, `CharP.pi`, `CharP.quotient_iff_le_ker_natCast`, `CharP.charP_iff_prime_eq_zero`, `MixedCharZero.reduce_to_maximal_ideal`, `CharP.quotient_iff`, `ringChar.eq_iff`, `ULift.charP`, `ringChar.charP`, `FirstOrder.Field.charP_iff_model_fieldOfChar`, `ModP.charP`

---

← Back to Index