Theorem Matrix.isHermitian_intCast

Modification history

2024-08-12 23:05
Mathlib/LinearAlgebra/Matrix/Hermitian.lean
feat: `Matrix.PosDef` on diagonal and numeric matrices (#13974) …
Added Matrix.isHermitian_intCastView on Github →