zpow_natCast_sub_one₀

Mathlib.Algebra.GroupWithZero.Units.Basic

URI: https://scilib.ai/kg/mathlib#zpow_natCast_sub_one₀

English

For a ≠ 0 and n ∈ ℕ, we have a^{(n-1)} = a^{n} / a.

Русский

Пусть a ≠ 0 и n ∈ ℕ. Тогда a^{(n-1)} = a^{n} / a.

LaTeX

$$$\forall a\neq 0,\forall n\in\mathbb{N}: a^{(n-1)} = a^{n} / a$$$

Lean4

theorem zpow_natCast_sub_one₀ (ha : a ≠ 0) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a := by simpa using zpow_sub₀ ha n 1

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

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

Разделы

Аффилиация

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