coeff_mk

Mathlib.RingTheory.WittVector.Truncated

URI: https://scilib.ai/kg/mathlib#TruncatedWittVector.coeff_mk

English

For x : Fin n → R and i : Fin n, (mk p x).coeff i = x i.

Русский

Для x : Fin n → R и i : Fin n, (mk p x).coeff i = x i.

LaTeX

$$$\\forall (x : Fin n \\to R) (i : Fin n), (\\mathrm{mk}\\ p\\ x).\\mathrm{coeff} i = x i$$$

Lean4

@[simp]
theorem coeff_mk (x : Fin n → R) (i : Fin n) : (mk p x).coeff i = x i :=
  rfl

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

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

Разделы

Аффилиация

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