Theorem Matrix.isHermitian_transpose_iff

Modification history

2026-03-28 13:52

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

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

Modified Matrix.isHermitian_transpose_iff View on Github →

2023-05-29 13:15

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

feat: port LinearAlgebra.Matrix.Hermitian (#4467)

Added Matrix.isHermitian_transpose_iff View on Github →