mirror_inj — Mathlib

English

Let p and q be polynomials over a semiring R. The mirror (reversal) operation on polynomials is injective, i.e. if the mirrors of p and q are equal, then p and q are equal.

Русский

Пусть p и q — полиномы над полускольпом R. Операция зеркалирования полинома сохраняет информацию о коэффициентах так, что если их зеркала совпадают, то сами полиномы совпадают.

LaTeX

$$$ p^{\\sim} = q^{\\sim} \\iff p = q $$$

Lean4

@[simp]
theorem mirror_inj : p.mirror = q.mirror ↔ p = q :=
  mirror_involutive.injective.eq_iff

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