Theorems · Definition · number theory
AddChar.IsPrimitive
{R : Type u} → [inst : CommRing R] → {R' : Type v} → [inst_1 : CommMonoid R'] → AddChar R R' → PropAn additive character is primitive iff all its multiplicative shifts by nonzero elements are nontrivial.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- CommRingCommMonoid
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.
- CommRingstatement and proof · cited by 17,173
- CommMonoidstatement and proof · cited by 2,264
- AddCharstatement and proof · cited by 286
- AddChar.mulShiftproof · cited by 26
Cited by27
Results whose statement or proof uses this declaration.
- AddChar.PrimitiveAddChar.primstatement · cited by 4
- gaussSum_mul_gaussSum_eq_cardstatement and proof · cited by 4
- AddChar.sum_mulShiftstatement and proof · cited by 2
- AddChar.zmod_char_primitive_of_eq_one_only_at_zerostatement · cited by 2
- AddChar.IsPrimitive.compMulHom_of_isPrimitivestatement and proof · cited by 1
- AddChar.IsPrimitive.zmod_char_eq_one_iffstatement and proof · cited by 1
- AddChar.PrimitiveAddChar.mk.injstatement and proof · cited by 1
- AddChar.PrimitiveAddChar.mk.noConfusionstatement and proof · cited by 1
- AddChar.exists_divisor_of_not_isPrimitivestatement and proof · cited by 1
- gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitivestatement and proof · cited by 1
- gaussSum_mul_gaussSum_pow_orderOf_sub_onestatement and proof · cited by 1
- gaussSum_ne_zero_of_nontrivialstatement and proof · cited by 1