npowRec'_succ

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#npowRec'_succ

← MathLib Explorer

English

For k ≠ 0, npowRec'(k+1) m = npowRec' k m · m.

Русский

Для k ≠ 0 верно: npowRec'(k+1) m = npowRec'(k) m · m.

LaTeX

$$$\\forall k,m:\\ k\\neq 0 \\Rightarrow npowRec'(k+1,m) = npowRec'(k,m) \\cdot m$$$

Lean4

@[to_additive]
theorem npowRec'_succ {M : Type*} [Mul M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) : npowRec' (k + 1) m = npowRec' k m * m :=
  match k with
  | _ + 1 => rfl

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

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

Разделы

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

Аффилиация

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