invOf — Mathlib

English

If x is algebraic over R and x is invertible in S, then 1/x is algebraic over R.

Русский

Если x алгебраичен над R и обратим в S, то x^{-1} алгебраичен над R.

LaTeX

$$$\forall {x : S} [\text{Invertible } x],\ \mathrm{IsAlgebraic}\ R\ x \Rightarrow \mathrm{IsAlgebraic}\ R\ (x^{-1})$$$

Lean4

theorem invOf {x : S} [Invertible x] (h : IsAlgebraic R x) : IsAlgebraic R (⅟x) :=
  by
  obtain ⟨p, hp, hp'⟩ := h
  refine ⟨p.reverse, by simpa using hp, ?_⟩
  rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]

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