coeff_out

Mathlib.RingTheory.WittVector.Truncated

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

← MathLib Explorer

English

The coeff of x.out at i equals the coeff of x at i.

Русский

Коэффициент x.out по i равен коэффициенту x по i.

LaTeX

$$$\\mathrm{TruncatedWittVector}.\\mathrm{coeff}\\ i\\ (x.out) = \\mathrm{TruncatedWittVector}.\\mathrm{coeff}\\ i\\ x$$$

Lean4

@[simp]
theorem coeff_out (x : TruncatedWittVector p n R) (i : Fin n) : x.out.coeff i = x.coeff i := by rw [out]; dsimp only;
  rw [dif_pos i.is_lt, Fin.eta]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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