of_finite — Mathlib

English

If A is a finite R-algebra, then A is algebraic over R (as an instance).

Русский

Если A — конечная над R алгебра, то A алгебраическая над R (инстанс).

LaTeX

$$$Module.Finite\ R\ A \Rightarrow Algebra.IsAlgebraic\ R\ A$$$

Lean4

/-- A field extension is algebraic if it is finite. -/
@[stacks 09GG "first part"]
instance of_finite [Module.Finite R A] : Algebra.IsAlgebraic R A :=
  (IsIntegral.of_finite R A).isAlgebraic

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