Theorems · Theorem · commutative algebra
CharP.charP_iff_prime_eq_zero
∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R] {p : ℕ}, Nat.Prime p → (CharP R p ↔ ↑p = 0)- Defined in
- Mathlib.Algebra.CharP.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocSemiringNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nontrivialstatement and proof · cited by 2,416
- Nat.Primestatement and proof · cited by 2,059
- NonAssocSemiringstatement and proof · cited by 805
- CharPstatement and proof · cited by 478
- CharP.cast_eq_zeroproof · cited by 357
- CharP.ringChar_of_prime_eq_zeroproof · cited by 2
Cited by4
Results whose statement or proof uses this declaration.
- FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realizeproof · cited by 2
- FirstOrder.Field.charP_iff_model_fieldOfCharproof · cited by 1
- charP_of_card_eq_prime_powproof · cited by 1
- charP_of_card_eq_primeproof · cited by 0