English
Let R be a semiring and M an R–module which is finite. For any submodule N of M (viewed suitably as an A–submodule in the given scalar-tower setting), the quotient M/N is finite as an R–module.
Русский
Пусть R — полускольная кольцо, и M — конечный как модуль над R. Для любого подпрародного подмодуля N модуля M (при корректном рассмотрении как A–модуля в данной схеме скаляров) получаем фактор-модуль M/N конечен как R-модуль.
LaTeX
$$$\\forall R\,A\,M\,N\\; [\\text{Semiring } R]\, [\\text{Ring } A]\, [\\text{Module } A M]\, [\\text{Module } R M]\, [\\text{SMul } R A]\, [\\text{IsScalarTower } R A M]\, [\\text{Module.Finite } R M]\\; \\Rightarrow\\; \\text{Module.Finite } R (M / N)$$$
Lean4
instance quotient (R) {A M} [Semiring R] [AddCommGroup M] [Ring A] [Module A M] [Module R M] [SMul R A]
[IsScalarTower R A M] [Module.Finite R M] (N : Submodule A M) : Module.Finite R (M ⧸ N) :=
Module.Finite.of_surjective (N.mkQ.restrictScalars R) N.mkQ_surjective
