Defs

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

Statistics

Metric	Count
Definitions `ExpChar`, `ringChar`, `ringExpChar`	3
Theorems `subsingleton`, `cast_eq_iff_mod_eq`, `cast_eq_mod`, `cast_eq_zero`, `cast_eq_zero_iff`, `charP_to_charZero`, `charP_zero_iff_charZero`, `char_is_prime_of_pos`, `char_is_prime_of_two_le`, `char_is_prime_or_zero`, `char_ne_one`, `char_prime_of_ne_zero`, `eq`, `exists`, `exists'`, `existsUnique`, `false_of_nontrivial_of_char_one`, `intCast_eq_zero_iff`, `neg_one_ne_one`, `nontrivial_of_char_ne_one`, `ofCharZero`, `ofNat_eq_zero`, `ofNat_eq_zero'`, `ringChar_ne_one`, `ringChar_zero_iff_CharZero`, `eq`, `exists`, `exists_unique`, `not_char_dvd`, `of_not_dvd`, `charP_iff`, `charZero_of_expChar_one'`, `char_eq_expChar_iff`, `char_zero_of_expChar_one`, `expChar_is_prime_or_one`, `expChar_ne_zero`, `expChar_one`, `expChar_one_iff_char_zero`, `expChar_one_of_char_zero`, `expChar_pos`, `expChar_pow_pos`, `expChar_prime`, `cast_ringChar`, `charP`, `dvd`, `eq`, `eq_iff`, `eq_zero`, `of_eq`, `ringChar_eq_one`, `ringChar_subsingleton`, `spec`, `eq`, `eq_iff`, `eq_one`, `expChar`, `of_eq`	57
Total	60

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_eq_iff_mod_eq` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`Nat.cast_add` `left_eq_add` `cast_eq_zero_iff` `add_zero` `LT.lt.le`
`cast_eq_mod` 📖	mathematical	—	`AddMonoidWithOne.toNatCast`	—	`cast_eq_zero_iff` `Nat.cast_add` `add_zero`
`cast_eq_zero` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_eq_zero_iff` `dvd_rfl`
`cast_eq_zero_iff` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	—
`charP_to_charZero` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne`	—	`charZero_of_inj_zero` `eq_zero_of_zero_dvd` `cast_eq_zero_iff`
`charP_zero_iff_charZero` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `CharZero`	—	`charP_to_charZero` `ofCharZero`
`char_is_prime_of_pos` 📖	mathematical	—	`Fact` `Nat.Prime`	—	`char_is_prime_or_zero`
`char_is_prime_of_two_le` 📖	mathematical	—	`Nat.Prime`	—	`cast_eq_zero_iff` `dvd_refl` `Nat.cast_mul` `NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `Dvd.dvd.antisymm'` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `dvd_of_mul_left_eq` `Dvd.dvd.antisymm` `mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero` `LT.lt.ne'` `Nat.prime_def`
`char_is_prime_or_zero` 📖	mathematical	—	`Nat.Prime`	—	`char_ne_one` `char_is_prime_of_two_le`
`char_ne_one` 📖	—	—	—	—	`NeZero.one` `Nat.cast_one` `cast_eq_zero_iff` `dvd_refl` `one_ne_zero`
`char_prime_of_ne_zero` 📖	mathematical	—	`Nat.Prime`	—	`char_is_prime_or_zero`
`eq` 📖	—	—	—	—	`cast_eq_zero_iff` `cast_eq_zero`
`exists` 📖	mathematical	—	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`by_cases` `zero_dvd_iff` `Nat.cast_zero` `by_contradiction` `Nat.find_min` `Nat.find_spec` `add_zero` `MulZeroClass.zero_mul` `of_not_not` `Nat.cast_mul` `Nat.cast_add`
`exists'` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Fact` `Nat.Prime` `CharP`	—	`exists` `char_is_prime_or_zero` `charP_to_charZero`
`existsUnique` 📖	mathematical	—	`ExistsUnique` `CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`exists` `eq`
`false_of_nontrivial_of_char_one` 📖	—	—	—	—	`CharOne.subsingleton` `false_of_nontrivial_of_subsingleton`
`intCast_eq_zero_iff` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup`	—	`lt_trichotomy` `neg_eq_zero` `Int.cast_neg` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `le_of_lt` `Int.cast_natCast` `cast_eq_zero_iff` `Int.cast_zero`
`neg_one_ne_one` 📖	—	—	—	—	`sub_ne_zero` `sub_neg_eq_add` `Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `Nat.cast_two` `cast_eq_zero_iff` `LT.lt.not_ge` `Fact.out`
`nontrivial_of_char_ne_one` 📖	mathematical	—	`Nontrivial`	—	`cast_eq_zero_iff`
`ofCharZero` 📖	mathematical	—	`CharP`	—	`zero_dvd_iff` `Nat.cast_zero`
`ofNat_eq_zero` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_eq_zero`
`ofNat_eq_zero'` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`cast_eq_zero_iff`
`ringChar_ne_one` 📖	—	—	—	—	`not_subsingleton`
`ringChar_zero_iff_CharZero` 📖	mathematical	—	`ringChar` `NonAssocRing.toNonAssocSemiring` `CharZero` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`ringChar.eq_iff` `charP_zero_iff_charZero`

CharP.CharOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton` 📖	—	—	—	—	`one_mul` `Nat.cast_one` `CharP.cast_eq_zero` `MulZeroClass.zero_mul`

ExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	—	—	—	—	`Nat.not_prime_zero` `CharP.eq` `CharP.ofCharZero`
`exists` 📖	mathematical	—	`ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`CharP.exists'` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial`
`exists_unique` 📖	mathematical	—	`ExistsUnique` `ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`exists` `eq`

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_char_dvd` 📖	—	—	—	—	`CharP.cast_eq_zero_iff`
`of_not_dvd` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`Iff.not` `CharP.cast_eq_zero_iff`

(root)

Definitions

Name	Category	Theorems
`ExpChar` 📖	CompData	23 math math: `ExpChar.expChar_center_iff`, `RingHom.expChar_iff`, `ExpChar.of_injective_algebraMap'`, `ringExpChar.eq_iff`, `ExpChar.congr`, `ringExpChar.of_eq`, `Polynomial.SplittingField.instExpChar`, `expChar_one`, `expChar_of_injective_ringHom`, `instExpCharProd`, `Polynomial.instExpChar`, `ringExpChar.expChar`, `IntermediateField.expChar`, `RatFunc.instExpChar`, `Subfield.expChar`, `expChar_of_injective_algebraMap`, `MvPolynomial.instExpChar`, `IntermediateField.expChar'`, `instExpCharLinearMapSubtypeMemSubringCenterId`, `RingHom.expChar`, `ExpChar.exists_unique`, `ExpChar.exists`, `expChar_prime`
`ringChar` 📖	CompOp	23 math math: `ringChar.ringChar_eq_one`, `ringChar.dvd`, `MulChar.map_ringChar`, `ringChar.eq`, `ringChar.ringChar_subsingleton`, `Algebra.ringChar_eq`, `prime_dvd_char_iff_dvd_card`, `CharP.ringChar_zero_iff_CharZero`, `CharP.prime_ringChar`, `not_ringChar_dvd_of_invertible`, `isUnit_iff_not_dvd_char`, `ringChar.Nat.cast_ringChar`, `ringChar.spec`, `orderOf_neg_one`, `isUnit_iff_not_dvd_char_of_ringChar_ne_zero`, `CharP.ringChar_of_prime_eq_zero`, `ZMod.ringChar_zmod_n`, `FiniteField.even_card_iff_char_two`, `Ideal.ringChar_quot`, `ringChar.eq_iff`, `neg_one_eq_one_iff`, `ringChar.charP`, `ringChar.eq_zero`
`ringExpChar` 📖	CompOp	14 math math: `ringExpChar.eq_one`, `ringExpChar.eq`, `IsPurelyInseparable.elemExponent_min`, `IsPurelyInseparable.hasExponent_iff`, `IsPurelyInseparable.minpoly_eq`, `IsPurelyInseparable.HasExponent.has_exponent`, `ringExpChar.eq_iff`, `mem_perfectClosure_iff`, `ringExpChar.expChar`, `IsPurelyInseparable.minpoly_natDegree_eq`, `IsPurelyInseparable.exponent_min`, `IsPurelyInseparable.algebraMap_elemReduct_eq`, `IsPurelyInseparable.exponent_def`, `IsPurelyInseparable.elemExponent_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP_iff` 📖	mathematical	—	`CharP` `AddMonoidWithOne.toNatCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	—
`charZero_of_expChar_one'` 📖	mathematical	—	`CharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`CharP.char_ne_one`
`char_eq_expChar_iff` 📖	mathematical	—	`Nat.Prime`	—	`CharP.eq` `CharP.ofCharZero`
`char_zero_of_expChar_one` 📖	—	—	—	—	`CharP.eq` `CharP.ofCharZero` `CharP.char_ne_one`
`expChar_is_prime_or_one` 📖	mathematical	—	`Nat.Prime`	—	—
`expChar_ne_zero` 📖	—	—	—	—	`one_ne_zero` `Nat.Prime.ne_zero`
`expChar_one` 📖	mathematical	—	`ExpChar`	—	—
`expChar_one_iff_char_zero` 📖	—	—	—	—	`char_zero_of_expChar_one` `expChar_one_of_char_zero`
`expChar_one_of_char_zero` 📖	—	—	—	—	`Nat.Prime.ne_zero` `CharP.eq`
`expChar_pos` 📖	—	—	—	—	`expChar_is_prime_or_one` `Nat.Prime.pos`
`expChar_pow_pos` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid`	—	`expChar_pos`
`expChar_prime` 📖	mathematical	—	`ExpChar`	—	`Fact.out`

ringChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ringChar`	—	`spec`
`dvd` 📖	mathematical	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`ringChar`	—	`spec`
`eq` 📖	mathematical	—	`ringChar`	—	`CharP.existsUnique`
`eq_iff` 📖	mathematical	—	`ringChar` `CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`of_eq` `eq`
`eq_zero` 📖	mathematical	—	`ringChar`	—	`eq` `CharP.ofCharZero`
`of_eq` 📖	mathematical	`ringChar`	`CharP` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`CharP.congr` `charP`
`ringChar_eq_one` 📖	mathematical	—	`ringChar`	—	`spec` `Nat.cast_one` `subsingleton_iff_zero_eq_one`
`ringChar_subsingleton` 📖	mathematical	—	`ringChar`	—	—
`spec` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ringChar`	—	`CharP.cast_eq_zero_iff` `CharP.existsUnique`

ringChar.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_ringChar` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `ringChar` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`ringChar.spec` `dvd_refl`

ringExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`ringExpChar`	—	`eq_1` `ringChar.eq` `CharP.ofCharZero` `LT.lt.le` `Nat.Prime.one_lt`
`eq_iff` 📖	mathematical	—	`ringExpChar` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`of_eq` `eq`
`eq_one` 📖	mathematical	—	`ringExpChar`	—	`eq_1` `ringChar.eq_zero` `max_eq_right`
`expChar` 📖	mathematical	—	`ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `ringExpChar` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	`ExpChar.exists` `eq`
`of_eq` 📖	mathematical	`ringExpChar` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	`ExpChar` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`expChar`

---

← Back to Index