tower_top — Mathlib

English

For invertible x, IsAlgebraic R x^{-1} iff IsAlgebraic R x.

Русский

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

LaTeX

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

Lean4

/-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
@[stacks 09GF "part two"]
theorem tower_top [Algebra.IsAlgebraic K A] : Algebra.IsAlgebraic L A :=
  Algebra.IsAlgebraic.extendScalars (algebraMap K L).injective

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