Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-07 15:21
8c52db32
View on Github →
feat: Trivial Star makes ConjTranspose_eq_transpose (
#6419
) Under the trivial star, $A^H = A^T$
Estimated changes
Modified
Mathlib/Data/Matrix/Basic.lean
added
theorem
Matrix.conjTranspose_eq_transpose_of_trivial