reflect_C

Mathlib.Algebra.Polynomial.Reverse

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

← MathLib Explorer

English

Reflect maps monomials as expected: reflect N (X^n) = X^{revAt N n}.

Русский

Reflect отображает мономиональные элементы как ожидалось: reflect N (X^n) = X^{revAt N n}.

LaTeX

$$$\\mathrm{reflect}\\ N\\ (X^n)=X^{\\mathrm{revAt}\\ N\\ n}.$$$

Lean4

@[simp]
theorem reflect_C (r : R) (N : ℕ) : reflect N (C r) = C r * X ^ N := by
  conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

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

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

Разделы

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

Аффилиация

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