Theorem Submodule.exists_forall_notMem_of_forall_ne_top

Modification history

2025-08-03 21:39
Mathlib/Algebra/Module/Submodule/Union.lean
feat: a finite union of proper submodules is a proper subset (#27598) …
Added Submodule.exists_forall_notMem_of_forall_ne_topView on Github →