Commit 2023-08-23 12:46 e9d747ef

View on Github →

chore(Data/Matrix/Invertible): generalize conjugate and transpose lemmas (#6618) The conjTranspose lemmas now work for non-commutative rings.

Estimated changes

Modified Mathlib/Data/Matrix/Invertible.lean

added theorem Matrix.conjTranspose_invOf

added def Matrix.invertibleOfInvertibleConjTranspose

added def Matrix.invertibleOfInvertibleTranspose

added theorem Matrix.isUnit_conjTranspose

added theorem Matrix.isUnit_transpose

added def Matrix.transposeInvertibleEquivInvertible

added theorem Matrix.transpose_invOf

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

deleted def Matrix.invertibleOfInvertibleConjTranspose

deleted def Matrix.invertibleOfInvertibleTranspose