opow_dvd_opow_iff — Mathlib

English

If a > 1, then a^b divides a^c if and only if b ≤ c.

Русский

Если a > 1, то a^b делит a^c тогда и только тогда, когда b ≤ c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ 1 < a \Rightarrow (a^{b} \mid a^{c} \iff b \le c)$$$

Lean4

theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c :=
  ⟨fun h =>
    le_of_not_gt fun hn =>
      not_le_of_gt ((opow_lt_opow_iff_right a1).2 hn) <| le_of_dvd (opow_ne_zero _ <| one_le_iff_ne_zero.1 <| a1.le) h,
    opow_dvd_opow _⟩

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