English
If n is nonzero and ζ is a primitive n-th root of unity in a domain, then n maps to a nonzero element in R.
Русский
Если n не нуль и ζ — примитивный корень n-й степени единицы в домене, то образ n в R не нулевой.
LaTeX
$$IsPrimitiveRoot(\\zeta, n) \\Rightarrow (n : R) \\neq 0$$
Lean4
theorem neZero' {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) : NeZero ((n : ℕ) : R) :=
by
let p := ringChar R
have hfin := Nat.finiteMultiplicity_iff.2 ⟨CharP.char_ne_one R p, NeZero.pos n⟩
obtain ⟨m, hm⟩ := hfin.exists_eq_pow_mul_and_not_dvd
by_cases hp : p ∣ n
· obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero (multiplicity_pos_of_dvd hp).ne'
have : NeZero p := NeZero.of_pos (Nat.pos_of_dvd_of_pos hp (NeZero.pos n))
have hpri : Fact p.Prime := CharP.char_is_prime_of_pos R p
have := hζ.pow_eq_one
rw [hm.1, hk, pow_succ', mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at this
exfalso
have hpos : 0 < p ^ k * m := mul_pos (pow_pos hpri.1.pos _) <| Nat.pos_of_ne_zero (fun H ↦ hm.2 <| H ▸ p.dvd_zero)
refine hζ.pow_ne_one_of_pos_of_lt hpos.ne' ?_ (frobenius_inj R p this)
rw [hm.1, hk, pow_succ', mul_assoc, mul_comm p]
exact lt_mul_of_one_lt_right hpos hpri.1.one_lt
· exact NeZero.of_not_dvd R hp
