shiftₗ

Mathlib.Algebra.Group.ForwardDiff

URI: https://scilib.ai/kg/mathlib#fwdDiff_aux.shiftₗ

Lean4

/-- Linear-endomorphism version of the shift-by-1 operator. -/
def shiftₗ : Module.End ℤ (M → G) :=
  fwdDiffₗ M G h + 1

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

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

Разделы

Аффилиация

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