Theorems · Theorem · commutative algebra

Submodule.exists_forall_notMem_of_forall_ne_top

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

Defined in

Mathlib.Algebra.Module.Submodule.Union

Cited by

1 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldAddCommGroupModuleFiniteInfinite