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