restriction_one

Mathlib.RingTheory.Polynomial.Basic

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

← MathLib Explorer

English

Restricting the constant polynomial 1 results in 1.

Русский

Ограничение константы 1 дает 1.

LaTeX

$$$\\mathrm{restriction}(1) = 1$$$

Lean4

@[simp]
theorem restriction_one : restriction (1 : R[X]) = 1 :=
  ext fun i => Subtype.eq <| by rw [coeff_restriction', coeff_one, coeff_one]; split_ifs <;> rfl

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

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

Разделы

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

Аффилиация

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