prod — Mathlib

English

If sb and sc are finitely generated submodules of modules, then their product sb.prod sc is finitely generated.

Русский

Если sb и sc — конечнопорожденные подмодули, то их произведение sb.prod sc также конечнопорождено.

LaTeX

$$$sb.FG \\land sc.FG \\Rightarrow (sb.prod sc).FG$$$

Lean4

theorem prod {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.FG) (hsc : sc.FG) : (sb.prod sc).FG :=
  let ⟨tb, htb⟩ := fg_def.1 hsb
  let ⟨tc, htc⟩ := fg_def.1 hsc
  fg_def.2
    ⟨LinearMap.inl R M P '' tb ∪ LinearMap.inr R M P '' tc, (htb.1.image _).union (htc.1.image _), by
      rw [LinearMap.span_inl_union_inr, htb.2, htc.2]⟩

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