Theorem Matrix.IsHermitian.of_subsingleton

Modification history

2025-12-01 20:13
Mathlib/LinearAlgebra/Matrix/Hermitian.lean
feat: add `IsHermitian.of_subsingleton` (#32314)
Added Matrix.IsHermitian.of_subsingletonView on Github →