repeat_apply

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.repeat_apply

English

Repeat a function a m times: Fin.repeat m a : Fin m → α maps i to a(i modNat).

Русский

Повторить функцию a m раз: Fin.repeat m a: Fin m → α отображает i в a(i modNat).

LaTeX

$$$\\mathrm{Fin.repeat}\\;m\\;a = \\lambda i. a(i \\bmodNat).$$$

Lean4

@[simp]
theorem repeat_apply (a : Fin n → α) (i : Fin (m * n)) : Fin.repeat m a i = a i.modNat :=
  rfl

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

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

Разделы

Аффилиация

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