instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite

English

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

Русский

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

LaTeX

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

Lean4

instance [Finite σ] (N : ℕ) : Module.Finite R (restrictTotalDegree σ R N) :=
  have := finite_setOf_bounded σ N
  have : Finite {s : σ →₀ ℕ | s.sum (fun _ e ↦ e) ≤ N} :=
    by
    rw [Set.finite_coe_iff] at this ⊢
    exact
      this.subset fun n hn i ↦
        (eq_or_ne (n i) 0).elim (fun h ↦ h.trans_le N.zero_le) fun h ↦
          (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn
  Module.Finite.of_basis (basisRestrictSupport R _)

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