Commit 2023-08-16 21:06 d72f88a7

View on Github →

chore: conjTranspose and transpose are obviously injective (#6615) conjTranspose and transpose are injective

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.conjTranspose_inj

added theorem Matrix.conjTranspose_injective

modified theorem Matrix.transpose_eq_zero

added theorem Matrix.transpose_inj

added theorem Matrix.transpose_injective