dvd_pow — Mathlib

English

Let α be a monoid and a, b ∈ α with a | b. Then for every natural number n > 0, a | b^n.

Русский

Пусть алгебраическая структура является моноидом, и a, b ∈ α удовлетворяют a | b. Тогда для любого n ∈ ℕ, n > 0, выполняется a | b^n.

LaTeX

$$$ (a \mid b) \rightarrow \forall {n : \mathbb{N}}, n \neq 0 \rightarrow a \mid b^{n}$$$

Lean4

theorem dvd_pow (hab : a ∣ b) : ∀ {n : ℕ} (_ : n ≠ 0), a ∣ b ^ n
  | 0, hn => (hn rfl).elim
  | n + 1, _ => by rw [pow_succ']; exact hab.mul_right _

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