Theorem LinearMap.exists_ne_zero_of_sSup_eq_top

Modification history

2025-05-01 06:42
Mathlib/Algebra/Module/Submodule/Ker.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added LinearMap.exists_ne_zero_of_sSup_eq_topView on Github →