Theorems · Theorem · number theory
AddChar.zmod_char_primitive_of_eq_one_only_at_zero
∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) (ψ : AddChar (ZMod n) C), (∀ (a : ZMod n), ψ a = 1 → a = 0) → ψ.IsPrimitiveThe converse: if the additive character takes the value 1 only at 0,
then it is primitive.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Quot.sound
- Assumes
- CommMonoid
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.
- DFunLike.coestatement and proof · cited by 62,936
- mul_oneproof · cited by 3,885
- Nat.cast_oneproof · cited by 2,501
- CommMonoidstatement and proof · cited by 2,264
- ZModstatement and proof · cited by 1,024
- AddCharstatement and proof · cited by 286
- AddChar.mulShiftproof · cited by 26
- AddChar.IsPrimitivestatement · cited by 22
- AddChar.mulShift_applyproof · cited by 9
Cited by2
Results whose statement or proof uses this declaration.
- ZMod.isPrimitive_stdAddCharproof · cited by 1
- AddChar.zmodChar_primitive_of_primitive_rootproof · cited by 0