instModuleFinite — Mathlib

English

If a module E is finite over a ring R with a linear order, then E is finite over the nonnegative subring R≥0.

Русский

Если модуль E конечно над кольцом R с линейным порядком, то он конечно же и над подкольцом неотрицательных скаляров R≥0.

LaTeX

$$$[\\text{Finite } R] \Rightarrow [\\text{Module.Finite } R_{\\ge 0} E].$$$

Lean4

/-- If a module is finite over a linearly ordered ring, then it is also finite over the non-negative
scalars. -/
instance instModuleFinite [Module.Finite R E] : Module.Finite R≥0 E :=
  .trans R E

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