Commit 2026-02-23 13:05 6eb4442a

View on Github →

chore(LinearAlgebra/Matrix/SemiringInverse): generalize from the identity to diagonal matrices (#35676) This is a trivial generalization of some helper lemmas.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

added theorem Matrix.detp_neg_one_diagonal

added theorem Matrix.detp_one_diagonal

modified theorem Matrix.isAddUnit_detp_mul_detp

modified theorem Matrix.isAddUnit_detp_smul_mul_adjp

modified theorem Matrix.isAddUnit_mul