isArtinian_pi' — Mathlib

English

Non-dependent version: the non-dependent product of Artinian modules is Artinian.

Русский

Независимая от индекса версия: не зависимое произведение артинанов должно быть артинановым.

LaTeX

$$$IsArtinian\\ R\\ M \\Rightarrow IsArtinian\\ R\\ (\\Pi\\ i, M)$$$

Lean4

/-- A version of `isArtinian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`). -/
instance isArtinian_pi' [IsArtinian R M] : IsArtinian R (ι → M) :=
  isArtinian_pi

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