Theorems · Theorem · commutative algebra
CharP.intCast_eq_zero_iff
∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] (a : ℤ), ↑a = 0 ↔ ↑p ∣ a
- Defined in
- Mathlib.Algebra.CharP.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroupWithOneCharP
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- le_of_ltproof · cited by 1,175
- CharPstatement and proof · cited by 478
- Int.cast_natCastproof · cited by 393
- Int.cast_negproof · cited by 224
- Int.cast_zeroproof · cited by 188
- lt_trichotomyproof · cited by 178
- neg_eq_zeroproof · cited by 171
- AddGroupWithOnestatement and proof · cited by 111
- CharP.cast_eq_zero_iffproof · cited by 42
Cited by7
Results whose statement or proof uses this declaration.
- Int.ModEq.pow_card_sub_one_eq_oneproof · cited by 3
- CharP.intCast_eq_intCastproof · cited by 3
- ZMod.castHom_injectiveproof · cited by 2
- ZMod.intCast_eq_zero_iff_evenproof · cited by 2
- MvPolynomial.C_dvd_iff_zmodproof · cited by 1
- prime_dvd_char_iff_dvd_cardproof · cited by 1
- CharP.ker_intAlgebraMap_eq_spanproof · cited by 0