isNoetherian_pi — Mathlib

English

If M is Noetherian and P is Noetherian, then the direct product M × P is Noetherian.

Русский

Если M и P — Noetherian, то их прямая сумма M × P — Noetherian.

LaTeX

$$$[IsNoetherian R M] \wedge [IsNoetherian R P] \Rightarrow IsNoetherian R (M \times P)$$$

Lean4

instance isNoetherian_pi :
    ∀ {M : ι → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] [∀ i, IsNoetherian R (M i)],
      IsNoetherian R (Π i, M i) :=
  by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

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