involutive_invert — Mathlib

English

Invert acts as an involution on Laurent polynomials: applying it twice yields the original Laurent polynomial. Formally, for every p, invert(invert(p)) = p.

Русский

Invert является инволюцией на лаурентовых полиномах: применение дважды возвращает исходный полином. Формально: для любого p выполняется invert(invert(p)) = p.

LaTeX

$$$ \forall p:\; \operatorname{invert}(\operatorname{invert}(p)) = p $$$

Lean4

theorem involutive_invert : Involutive (invert (R := R)) := fun _ ↦ by ext; simp

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