Theorems · Theorem · number theory
ZMod.natCast_val
∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [NeZero n] (i : ZMod n), ↑i.val = i.cast- Defined in
- Mathlib.Data.ZMod.Basic
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- ZModstatement and proof · cited by 1,024
- ZMod.valstatement · cited by 159
- ZMod.caststatement · cited by 87
- ZMod.natCast_comp_valproof · cited by 1
Cited by27
Results whose statement or proof uses this declaration.
- ZMod.unitsMap_surjectiveproof · cited by 7
- ZMod.val_intCastproof · cited by 5
- PadicInt.appr_specproof · cited by 4
- ZMod.wilsons_lemmaproof · cited by 2
- ZMod.intCast_eq_iffproof · cited by 2
- PadicInt.pow_dvd_nthHom_subproof · cited by 2
- gaussSum_aux_of_mulShiftproof · cited by 1
- summable_indicator_mod_iff_summable_indicator_modproof · cited by 1
- DirichletCharacter.factorsThrough_gcdproof · cited by 1
- IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_applyproof · cited by 1
- ZMod.cast_neg_oneproof · cited by 1
- ZMod.eq_unit_mul_divisorproof · cited by 1