pow_sub_one_mul

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

If n ≠ 0, then a^{n-1} · a = a^{n}.

Русский

Если n ≠ 0, то a^{n-1} · a = a^{n}.

LaTeX

$$$n \\neq 0 \\Rightarrow a^{n-1} \\cdot a = a^{n}$$$

Lean4

@[to_additive add_sub_one_nsmul]
theorem pow_sub_one_mul (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n := by
  rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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