natCast_comp

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

For any natural n, the constant polynomial n, composed with p, equals n.

Русский

Для любого натурального n константный полином n при композиции с p даёт тот же константный полином n.

LaTeX

$$(n : R[X]).comp p = n$$

Lean4

@[simp]
theorem natCast_comp {n : ℕ} : (n : R[X]).comp p = n := by rw [← C_eq_natCast, C_comp]

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

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

Разделы

Аффилиация

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