invOf_iff — Mathlib

English

For invertible x, IsAlgebraic R x^{-1} holds if and only if IsAlgebraic R x.

Русский

Для обратимого элемента x справедливо: IsAlgebraic R x^{-1} эквивалентно IsAlgebraic R x.

LaTeX

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

Lean4

theorem invOf_iff {x : S} [Invertible x] : IsAlgebraic R (⅟x) ↔ IsAlgebraic R x :=
  ⟨IsAlgebraic.invOf, IsAlgebraic.invOf⟩

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