Unions of Submodules

This file is a home for results about unions of submodules.

Main results:

• Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt: a finite union of proper submodules is a proper subset, provided the coefficients are a sufficiently large field.

theorem Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] (s : Finset ι) (p : ι → Submodule K M) (h₁ : ∀ (i : ι), p i ≠ ⊤) (h₂ : ↑s.card < ENat.card K) : ⋃ i ∈ s, ↑(p i) ⊂ Set.univ

theorem Submodule.exists_forall_notMem_of_forall_ne_top {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (p : ι → Submodule K M) (h : ∀ (i : ι), p i ≠ ⊤) : ∃ (x : M), ∀ (i : ι), x ∉ p i

theorem Module.Dual.exists_forall_ne_zero_of_forall_exists {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (f : ι → Dual K M) (h : ∀ (i : ι), ∃ (x : M), (f i) x ≠ 0) : ∃ (x : M), ∀ (i : ι), (f i) x ≠ 0

theorem Module.Dual.exists_forall_mem_ne_zero_of_forall_exists {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Finite ι] [Infinite K] (p : Submodule K M) (f : ι → Dual K M) (h : ∀ (i : ι), ∃ x ∈ p, (f i) x ≠ 0) : ∃ x ∈ p, ∀ (i : ι), (f i) x ≠ 0

A convenience variation of Module.Dual.exists_forall_ne_zero_of_forall_exists where we are concerned only about behaviour on a fixed submodule.