reflect_one

Mathlib.Algebra.Polynomial.Reverse

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

English

Reflect of 1 is X^n: reflect n 1 = X^n.

Русский

Reflect от единицы даёт X^n: reflect n 1 = X^n.

LaTeX

$$$\\mathrm{reflect}\\ n\\ 1 = X^{n}.$$$

Lean4

@[simp]
theorem reflect_one (n : ℕ) : (1 : R[X]).reflect n = Polynomial.X ^ n := by
  rw [← C.map_one, reflect_C, map_one, one_mul]

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

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

Разделы

Аффилиация

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