contract_C

Mathlib.Algebra.Polynomial.Expand

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

English

For every r in R, contracting the constant polynomial C(r) by p yields C(r): contraction fixes constants.

Русский

Для любого элемента r из R сжатие константного полиномa C(r) по p возвращает C(r).

LaTeX

$$$$\mathrm{contract}_p\bigl(C(r)\bigr)=C(r)$$$$

Lean4

@[simp]
theorem contract_C (r : R) : contract p (C r) = C r := by simp [contract]

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

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

Разделы

Аффилиация

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