mk_coeff

Mathlib.RingTheory.WittVector.Truncated

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

English

mk p (fun i => x.coeff i) recovers x.

Русский

Mk p fun i => x.coeff i восстанавливает x.

LaTeX

$$$\\mathrm{mk}\\ p\\ (\\lambda i. x.c\\oeff i) = x$$$

Lean4

@[simp]
theorem mk_coeff (x : TruncatedWittVector p n R) : (mk p fun i => x.coeff i) = x := by ext i; rw [coeff_mk]

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

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

Разделы

Аффилиация

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