not_isPrimitive_mulShift — Mathlib

English

Over a finite ring, if r is not a unit, then the additive character e.mulShift r is not primitive.

Русский

В конечном кольце, если r не единица, то e.mulShift r не примитивна.

LaTeX

$$¬IsUnit(r) → ¬IsPrimitive(e.mulShift r)$$

Lean4

/-- If `r` is not a unit, then `e.mulShift r` is not primitive. -/
theorem not_isPrimitive_mulShift [Finite R] (e : AddChar R R') {r : R} (hr : ¬IsUnit r) : ¬IsPrimitive (e.mulShift r) :=
  by
  simp only [IsPrimitive, not_forall]
  simp only [isUnit_iff_mem_nonZeroDivisors_of_finite, mem_nonZeroDivisors_iff_right, not_forall] at hr
  rcases hr with ⟨x, h, h'⟩
  exact ⟨x, h', by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]⟩

Похожие утверждения