isArtinian_prod — Mathlib

English

If M and P are Artinian over R, then their product M × P is Artinian.

Русский

Если M и P артинановы над R, то их произведение M × P артинаново.

LaTeX

$$$IsArtinian\\ R\\ M \\land IsArtinian\\ R\\ P \\Rightarrow IsArtinian\\ R\\ (M \\times P)$$$

Lean4

instance isArtinian_prod [IsArtinian R M] [IsArtinian R P] : IsArtinian R (M × P) :=
  isArtinian_of_range_eq_ker (LinearMap.inl R M P) (LinearMap.snd R M P) (LinearMap.range_inl R M P)

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