inv_iff — Mathlib

English

In a field K with R-algebra structure, for any x ≠ 0, IsAlgebraic R x^{-1} holds if and only if IsAlgebraic R x.

Русский

В поле K с структурой алгебры над R, для любого x ≠ 0, IsAlgebraic R x^{-1} эквивалентно IsAlgebraic R x.

LaTeX

$$$\forall {K} [\mathrm{Field}\ K] [\mathrm{Algebra}\ R\ K],\ \forall x\in K, x \neq 0:\ \mathrm{IsAlgebraic}\ R\ (x^{-1}) \iff \mathrm{IsAlgebraic}\ R\ x$$$

Lean4

theorem inv_iff {K} [Field K] [Algebra R K] {x : K} : IsAlgebraic R (x⁻¹) ↔ IsAlgebraic R x :=
  by
  by_cases hx : x = 0
  · simp [hx]
  letI := invertibleOfNonzero hx
  exact IsAlgebraic.invOf_iff (R := R) (x := x)

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