xInTermsOfW_zero

Mathlib.RingTheory.WittVector.WittPolynomial

URI: https://scilib.ai/kg/mathlib#xInTermsOfW_zero

← MathLib Explorer

English

If p is invertible in R, then xInTermsOfW p R 0 = X 0.

Русский

Если p обратимо в R, то xInTermsOfW p R 0 = X_0.

LaTeX

$$$ xInTermsOfW p R 0 = X 0 $$$

Lean4

@[simp]
theorem xInTermsOfW_zero [Invertible (p : R)] : xInTermsOfW p R 0 = X 0 := by
  rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]

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

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

Разделы

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

Аффилиация

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