Theorems · Theorem · number theory
AddChar.exists_divisor_of_not_isPrimitive
∀ {N : ℕ} [NeZero N] {R : Type u_1} [inst : CommRing R] (e : AddChar (ZMod N) R),
¬e.IsPrimitive → ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1If e is not primitive, then e.mulShift d = 1 for some proper divisor d of N.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- mul_commproof · cited by 2,262
- MulZeroClass.mul_zeroproof · cited by 2,091
- mul_assocproof · cited by 1,667
- IsUnitproof · cited by 1,602
- ZModstatement and proof · cited by 1,024
- AddCharstatement and proof · cited by 286
- lt_of_le_of_neproof · cited by 230
- NeZero.posproof · cited by 57
- AddChar.mulShiftstatement and proof · cited by 26
- AddChar.IsPrimitivestatement and proof · cited by 22
Cited by1
Results whose statement or proof uses this declaration.
- gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitiveproof · cited by 1