English
If e is not primitive, there exists a divisor d of N with d|N, d < N, and e.mulShift d = 1.
Русский
Если e не примитивна, существует делитель d числа N с d | N, d < N и e.mulShift d = 1.
LaTeX
$$∃ d ∣ N, d < N ∧ e.mulShift(d) = 1$$
Lean4
/-- If `e` is not primitive, then `e.mulShift d = 1` for some proper divisor `d` of `N`. -/
theorem exists_divisor_of_not_isPrimitive (he : ¬e.IsPrimitive) : ∃ d : ℕ, d ∣ N ∧ d < N ∧ e.mulShift d = 1 :=
by
simp_rw [IsPrimitive, not_forall, not_ne_iff] at he
rcases he with
⟨b, hb_ne, hb⟩
-- We have `AddChar.mulShift e b = 1`, but `b ≠ 0`.
obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor
refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩
· exact fun h ↦ by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne
· rw [← mulShift_unit_eq_one_iff _ hu, ← hb, mul_comm]
ext1 y
rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]
