mirror_zero

Mathlib.Algebra.Polynomial.Mirror

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

English

The mirror of a constant polynomial C a is itself.

Русский

Зеркало константного полинома C a равно самому C a.

LaTeX

$$$ (C a).mirror = C a $$$

Lean4

@[simp]
theorem mirror_zero : (0 : R[X]).mirror = 0 := by simp [mirror]

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

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

Разделы

Аффилиация

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