dvd_pow_self

Mathlib.Algebra.Divisibility.Basic

URI: https://scilib.ai/kg/mathlib#dvd_pow_self

English

For any a in a monoid and any nonzero n, a divides a^n.

Русский

Для любого элемента a моноида и любого n ≠ 0 верно: a делит a^n.

LaTeX

$$$ \forall a \,\in \; \alpha, \forall n \in \mathbb{N}, n \neq 0 \Rightarrow a \mid a^{n}$$$

Lean4

theorem dvd_pow_self (a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n :=
  dvd_rfl.pow hn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru