Theorem Matrix.isHermitian_comp_iff_forall

Modification history

2026-03-28 13:52

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

feat(LinearAlgebra/Matrix): expand `IsSymm`/`IsHermitian` API (#36349)

Added Matrix.isHermitian_comp_iff_forall View on Github →