Finite suprema of finite modules

instance Submodule.finite_iSup {R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)] : Module.Finite R ↥(⨆ (i : ι), S i)

The submodule generated by a supremum of finite dimensional submodules, indexed by a finite sort is finite-dimensional.

Equations

• ⋯ = ⋯