English
Let α be CancelCommMonoidWithZero. If a ≠ 0 and a is not a unit, then a^n divides a^m if and only if n ≤ m, for natural numbers n,m.
Русский
Пусть α — CancelCommMonoidWithZero. Если a ≠ 0 и не является единицей, то a^n делится на a^m тогда и только если n ≤ m, для натуральных n,m.
LaTeX
$$$a \\neq 0 \\land \\lnot IsUnit(a) \\Rightarrow (a^n \\mid a^m \\iff n \\le m)$$$
Lean4
theorem pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ n ≤ m :=
by
constructor
· intro h
rw [← not_lt]
intro hmn
apply ha
have : a ^ m * a ∣ a ^ m * 1 := by
rw [← pow_succ, mul_one]
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
apply pow_ne_zero m ha₀
· apply pow_dvd_pow
