isNoetherian_sup — Mathlib

English

If M1 and M2 are Noetherian submodules, then their supremum M1 ⊔ M2 is Noetherian.

Русский

Если подмодули M1 и M2 являются Noetherian, то их сумма M1 ⊔ M2 также Noetherian.

LaTeX

$$$[IsNoetherian R M_1] \wedge [IsNoetherian R M_2] \Rightarrow IsNoetherian R (M_1 \lor M_2)$$$

Lean4

instance isNoetherian_sup (M₁ M₂ : Submodule R P) [IsNoetherian R M₁] [IsNoetherian R M₂] : IsNoetherian R ↥(M₁ ⊔ M₂) :=
  by
  have := isNoetherian_range (M₁.subtype.coprod M₂.subtype)
  rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this

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