small_sup — Mathlib

English

If P and Q are finitely generated submodules of M over R, then their join P ⊔ Q (which is P + Q) is also finitely generated.

Русский

Пусть P и Q — конечнопорожденные подмодули M над R, тогда их сумма P ⊔ Q также конечнопорожденна.

LaTeX

$$$\operatorname{FG}(P) \land \operatorname{FG}(Q) \Rightarrow \operatorname{FG}(P+Q)$$$

Lean4

instance small_sup {P Q : Submodule R M} [smallP : Small.{u} P] [smallQ : Small.{u} Q] :
    Small.{u} (P ⊔ Q : Submodule R M) := by
  rw [Submodule.sup_eq_range]
  exact small_range _

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