Theorems · Theorem · number theory
ZMod.natCast_eq_zero_iff
∀ (a b : ℕ), ↑a = 0 ↔ b ∣ a
- Defined in
- Mathlib.Data.ZMod.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.cast_zeroproof · cited by 1,870
- ZModstatement and proof · cited by 1,024
- Nat.modEq_zero_iff_dvdproof · cited by 17
- ZMod.natCast_eq_natCast_iffproof · cited by 13
Cited by10
Results whose statement or proof uses this declaration.
- PadicInt.ker_toZModPowproof · cited by 3
- Polynomial.coprime_of_root_cyclotomicproof · cited by 2
- IsPrimitiveRoot.separable_minpoly_modproof · cited by 2
- Finset.univ_of_card_le_threeproof · cited by 1
- Nat.pow_pow_add_primeFactors_one_ltproof · cited by 1
- IsPrimitiveRoot.minpoly_eq_powproof · cited by 1
- Nat.prime_of_fac_equiv_neg_oneproof · cited by 1
- ZMod.neg_eq_self_iffproof · cited by 1
- ZMod.one_eq_zero_iffproof · cited by 0
- Nat.fermat_primeFactors_one_ltproof · cited by 0