npowRec_succ

Mathlib.Algebra.Group.Defs

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

English

For a semigroup with one, npowRec(n+1, a) = a · npowRec(n, a).

Русский

Для полугруппы с единицей, npowRec(n+1, a) = a · npowRec(n, a).

LaTeX

$$$\\forall n\\in\\mathbb{N},\\forall a\\in M:\\ npowRec(n+1,a) = a \\cdot npowRec(n,a).$$$

Lean4

@[to_additive]
theorem npowRec_succ : npowRec (n + 1) a = a * npowRec n a := by
  rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]

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

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

Разделы

Аффилиация

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