Note: some results should go to LinearAlgebra.Span.

theorem Submodule.sup_eq_span_union {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Submodule R M) : s ⊔ t = span R (↑s ∪ ↑t)

theorem Submodule.sup_eq_top_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Submodule R M) : s ⊔ t = ⊤ ↔ ∀ (m : M), ∃ u ∈ s, ∃ v ∈ t, m = u + v

theorem LinearMap.injective_iff_of_direct_sum {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {p q : Submodule R M} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (hpq : p ⊓ q = ⊥) (hpq' : p ⊔ q = ⊤) : Function.Injective ⇑f ↔ Disjoint p (ker f) ∧ Disjoint q (ker f) ∧ Disjoint (Submodule.map f p) (Submodule.map f q)

theorem LinearMap.ker_inf_eq_bot {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : ker f ⊓ S = ⊥ ↔ Set.InjOn ⇑f ↑S