of_finite

Mathlib.RingTheory.Algebraic.Integral

URI: https://scilib.ai/kg/mathlib#IsAlgebraic.of_finite

English

If A is finite as an R-module, then A is algebraic over R.

Русский

Если A конечномерно как модуль над R, то A алгебраическая над R.

LaTeX

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

Lean4

theorem of_finite (e : A) [Module.Finite R A] : IsAlgebraic R e :=
  (IsIntegral.of_finite R e).isAlgebraic

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru