natCast_opow_omega0 — Mathlib

English

For any a, b, if a ≠ 0 and b is multiplicatively principal with b > 2, then a·b = b^{succ(log_b a)}.

Русский

Для любых a, b, если a ≠ 0 и b — главный по умножению при b > 2, то a·b = b^{succ(log_b a)}.

LaTeX

$$$a \neq 0 \Rightarrow \operatorname{Principal}(\cdot * \cdot)\ b \land 2 < b \Rightarrow a \cdot b = b^{\operatorname{succ}(\log_b a)}$$$

Lean4

theorem natCast_opow_omega0 {n : ℕ} (hn : 1 < n) : n ^ ω = ω :=
  opow_omega0 (mod_cast hn) (nat_lt_omega0 n)

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