isTorsion_of_finiteDimensional — Mathlib

English

Let K be a field and A a finite-dimensional K-algebra acting on an additive group M that is finite-dimensional over K, with IsScalarTower. Then AEval K M a is a torsion module over the polynomial ring K[X].

Русский

Пусть K — поле, A — конечномерная над K алгебра, действующая на конечномерное по размерности пространство M над K. Тогда AEval K M a является торсионным модулем над K[X].

LaTeX

$$$\text{IsTorsion } K[X] (AEval\ K\ M\ a).$$$

Lean4

theorem isTorsion_of_finiteDimensional [Field K] [Ring A] [Algebra K A] [AddCommGroup M] [Module A M] [Module K M]
    [IsScalarTower K A M] [FiniteDimensional K A] : IsTorsion K[X] (AEval K M a) :=
  isTorsion_of_aeval_eq_zero (minpoly.aeval K a) (minpoly.ne_zero_of_finite K a)

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