Theorem LinearMap.ne_zero_of_surjective

Modification history

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