of_linearDisjoint_fg — Mathlib

English

If for every finitely generated submodule N' of N, N' ≤ N and N'.FG, we have M LinearDisjoint N', then M LinearDisjoint N.

Русский

Если для каждого конечноблочного подмодуля N' подмодуля N выполняется линейная несовместность с M, то M и N несовместны.

LaTeX

$$∀ N' ≤ N, N'.FG → M.LinearDisjoint N' → M.LinearDisjoint N$$

Lean4

/-- If for any finitely generated submodules `M'` and `N'` of `M` and `N`, respectively,
`M'` and `N'` are linearly disjoint, then `M` and `N` themselves are linearly disjoint. -/
theorem of_linearDisjoint_fg (H : ∀ (M' N' : Submodule R S), M' ≤ M → N' ≤ N → M'.FG → N'.FG → M'.LinearDisjoint N') :
    M.LinearDisjoint N :=
  of_linearDisjoint_fg_left _ _ fun _ hM hM' ↦ of_linearDisjoint_fg_right _ _ fun _ hN hN' ↦ H _ _ hM hN hM' hN'

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