instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite

English

If σ is finite, then the subtype of restrictDegree(σ,R,N) is a finite R-submodule.

Русский

Если σ конечен, то подмножество (Subtype) restrictDegree σ R N является конечным R-подмодулем.

LaTeX

$$$\\text{Module.Finite}\\; R\\; (\\mathrm{Subtype}\\ (x\\mapsto x\\in \\mathrm{restrictDegree}(\\sigma,R,N)))$$$

Lean4

instance [Finite σ] (N : ℕ) : Module.Finite R (restrictDegree σ R N) :=
  have := finite_setOf_bounded σ N
  Module.Finite.of_basis (basisRestrictSupport R _)

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