Theorem Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt

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.iUnion_ssubset_of_forall_ne_top_of_card_ltView on Github →