invert_C — Mathlib

English

Let R be a commutative semiring. For every t ∈ R, the constant Laurent polynomial C t is fixed by inversion: invert(C t) = C t.

Русский

Пусть R — коммутативное полукольцо. Тогда для любого t ∈ R константный лорантовский многочлен C(t) инвариант относительно операции invert: invert(C t) = C t.

LaTeX

$$$ \forall t \in R:\; \operatorname{invert}(C t) = C t $$$

Lean4

@[simp]
theorem invert_C (t : R) : invert (C t) = C t := by ext; simp

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