Theorem LinearMap.exists_ne_zero_of_sSup_eq

Modification history

2025-05-01 06:42
Mathlib/LinearAlgebra/Span/Basic.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added LinearMap.exists_ne_zero_of_sSup_eqView on Github →