reflect_one_X

Mathlib.Algebra.Polynomial.Reverse

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

English

Reflect of X is the image of X under the fixed N: reflect 1 (X) equals 1.

Русский

Reflect X при N=1 возвращает константу 1.

LaTeX

$$$\\mathrm{reflect}\\ 1\\ (X)=1.$$$

Lean4

@[simp]
theorem reflect_one_X : reflect 1 (X : R[X]) = 1 := by simpa using reflect_monomial 1 1 (R := R)

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

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

Разделы

Аффилиация

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