Commit 2024-06-21 18:31 b732d172

View on Github →

feat: more matrix lemmas about 37 : Matrix n n R etc (#13976) This extends the lemmas about zero and one in this file to lemmas about ofNat, natCast, and intCast.

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.conjTranspose_eq_diagonal

added theorem Matrix.conjTranspose_eq_intCast

added theorem Matrix.conjTranspose_eq_natCast

added theorem Matrix.conjTranspose_eq_ofNat

added theorem Matrix.conjTranspose_intCast

added theorem Matrix.conjTranspose_natCast

added theorem Matrix.conjTranspose_ofNat

added theorem Matrix.transpose_eq_diagonal

added theorem Matrix.transpose_eq_intCast

added theorem Matrix.transpose_eq_natCast

added theorem Matrix.transpose_eq_ofNat

added theorem Matrix.transpose_intCast

added theorem Matrix.transpose_natCast

added theorem Matrix.transpose_ofNat

modified theorem Matrix.transpose_one

modified theorem Matrix.transpose_zero