coeff_natCast_ite

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.coeff_natCast_ite

← MathLib Explorer

English

The coefficient of Nat.cast m in R[X] satisfies (Nat.cast m).coeff n = ite(n = 0) m 0.

Русский

Коэффициент nat_cast m в R[X] удовлетворяет (Nat.cast m).coeff n = ite(n = 0) m 0.

LaTeX

$$$ (\\mathrm{Nat.cast}\\, m).coeff(n) = \\mathrm{ite}(n = 0)\\, m\\, 0 $$$

Lean4

@[simp]
theorem coeff_natCast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
  simp only [← C_eq_natCast, coeff_C, Nat.cast_ite, Nat.cast_zero]

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

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

Разделы

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

Аффилиация

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