Theorems · Theorem · commutative algebra
CharP.exists
∀ (R : Type u_1) [inst : NonAssocSemiring R], ∃ p, CharP R p
- Defined in
- Mathlib.Algebra.CharP.Defs
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_zeroproof · cited by 2,707
- Nat.cast_zeroproof · cited by 1,870
- MulZeroClass.zero_mulproof · cited by 1,625
- NonAssocSemiringstatement and proof · cited by 805
- Nat.cast_addproof · cited by 586
- CharPstatement · cited by 478
- Nat.cast_mulproof · cited by 309
- Nat.findproof · cited by 139
- Nat.find_specproof · cited by 74
- of_not_notproof · cited by 51
- by_contradictionproof · cited by 42
- zero_dvd_iffproof · cited by 37
Cited by16
Results whose statement or proof uses this declaration.
- FiniteField.expand_cardproof · cited by 2
- FiniteField.Matrix.charpoly_pow_cardproof · cited by 2
- RingHom.charPproof · cited by 2
- CharP.exists'proof · cited by 2
- CharP.existsUniqueproof · cited by 2
- split_by_characteristicproof · cited by 2
- CharP.of_ringHom_of_ne_zeroproof · cited by 2
- charP_of_prime_pow_injectiveproof · cited by 1
- Ideal.exists_prime_and_absNorm_eq_powproof · cited by 1
- Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_Xproof · cited by 1
- IsArithFrobAt.exists_of_isInvariantproof · cited by 1
- FiniteField.card'proof · cited by 1