Theorems · Theorem · number theory

AddChar.not_isPrimitive_mulShift

∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] [Finite R] (e : AddChar R R') {r : R},
  ¬IsUnit r → ¬(e.mulShift r).IsPrimitive

If r is not a unit, then e.mulShift r is not primitive.

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommMonoidFinite