pow_inj — Mathlib

English

If i,j < k and ζ^i = ζ^j, then i = j.

Русский

Если i,j < k и ζ^i = ζ^j, то i = j.

LaTeX

$$$IsPrimitiveRoot(\zeta,k) \Rightarrow \forall i,j

Lean4

theorem pow_inj (h : IsPrimitiveRoot ζ k) ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) : i = j :=
  by
  wlog hij : i ≤ j generalizing i j
  · exact (this hj hi H.symm (le_of_not_ge hij)).symm
  apply le_antisymm hij
  rw [← tsub_eq_zero_iff_le]
  apply Nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj)
  apply h.dvd_of_pow_eq_one
  rw [← ((h.isUnit (Nat.ne_zero_of_lt hi)).pow i).mul_left_inj, ← pow_add, tsub_add_cancel_of_le hij, H, one_mul]

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