Theorem Module.Dual.exists_forall_ne_zero_of_forall_exists

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 Module.Dual.exists_forall_ne_zero_of_forall_existsView on Github →