isNoetherian_linearMap_pi — Mathlib

English

If ι is finite and M is Noetherian, then the space of linear maps from an ι-indexed copy of R into M is Noetherian.

Русский

Если ι конечен и M Noetherian, то пространство линейных отображений из (ι → R) в M Noetherian.

LaTeX

$$$[Finite ι] \Rightarrow IsNoetherian R ((ι \to R) \to_{R} M)$$$

Lean4

instance isNoetherian_linearMap_pi {ι : Type*} [Finite ι] : IsNoetherian R ((ι → R) →ₗ[R] M) :=
  let _i : Fintype ι := Fintype.ofFinite ι;
  isNoetherian_of_linearEquiv (Module.piEquiv ι R M)

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