English
If M is finite as an R-module and M carries an A-module structure compatible with R via a scalar tower, then M is finite as an A-module.
Русский
Если M конечен как модуль над R и имеется совместимая структура A-модуля через дерево скаляров, то M конечен как A-модуль.
LaTeX
$$$\\forall R\\, A\\, M\\; [\\text{Semiring } R] [\\text{Semiring } A] [\\text{Module } R M] [\\text{Module } A M] [\\text{SMul } R A] [\\text{IsScalarTower } R A M] [\\text{Module.Finite } R M],\\; \\text{Module.Finite } A M$$$
Lean4
theorem of_restrictScalars_finite (R A M : Type*) [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M]
[SMul R A] [IsScalarTower R A M] [hM : Module.Finite R M] : Module.Finite A M :=
by
rw [finite_def, Submodule.fg_def] at hM ⊢
obtain ⟨S, hSfin, hSgen⟩ := hM
refine ⟨S, hSfin, eq_top_iff.2 ?_⟩
have := Submodule.span_le_restrictScalars R A S
rwa [hSgen] at this
