Intersection_and_Sum_of_Submodules
Provedlatticelinear-algebramodulesproofwikisubmodules
Let be an -module. Let and be submodules of . Then and are also submodules of . The intersection of any set of submodules of is a submodule. Thus if , the intersection of all submodules of containing is the smallest submodule of containing .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Intersection_and_Sum_of_Submodules {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] (H K : Submodule R M) : H ⊓ K ≤ H ⊔ K := by sorrySource