toFinsupp_intCast

Mathlib.Algebra.Polynomial.Basic

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

English

The finsupp representation of the constant polynomial z equals z

Русский

Представление в Finsupp константного полинома z равно z

LaTeX

$$$ (z : R[X]).toFinsupp = z$$$

Lean4

@[simp]
theorem toFinsupp_intCast (z : ℤ) : (z : R[X]).toFinsupp = z :=
  rfl

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

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

Разделы

Аффилиация

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