pow_injective_of_not_isUnit — Mathlib

English

If q is not a unit and not zero, the map n ↦ q^n is injective.

Русский

Если q не единица и не ноль, отображение n ↦ q^n инъективно.

LaTeX

$$$\\forall q:\\, M,\\; \\lnot \\operatorname{IsUnit}(q) \\land q \\neq 0 \\Rightarrow \\operatorname{Injective}(n \\mapsto q^n).$$$

Lean4

theorem pow_injective_of_not_isUnit [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) :
    Function.Injective fun n : ℕ => q ^ n :=
  by
  refine injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
  · exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
  · exact (pow_mul_pow_sub q h.le).symm

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