zsmul

Mathlib.RingTheory.Algebraic.Integral

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

English

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

Русский

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

LaTeX

$$[Module.Finite R A] ⇒ Algebra.IsAlgebraic R A$$

Lean4

protected theorem zsmul (n : ℤ) : IsAlgebraic R (n • a) :=
  Int.cast_smul_eq_zsmul R n a ▸ ha.smul _

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

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

Разделы

Аффилиация

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