mirror_eq_iff

Mathlib.Algebra.Polynomial.Mirror

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

English

For polynomials p and q, p.mirror = q if and only if p = q.mirror.

Русский

Для многочленов p и q верно: p.mirror = q тогда и только тогда, когда p = q.mirror.

LaTeX

$$$ p.mirror = q \iff p = q.mirror $$$

Lean4

theorem mirror_eq_iff : p.mirror = q ↔ p = q.mirror :=
  mirror_involutive.eq_iff

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

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

Разделы

Аффилиация

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