Commit 2024-12-11 06:10 9eb9253e

View on Github →

feat(LinearAlgebra/Matrix): Prove A * B = 1 ↔ B * A = 1 for square matrices over a commutative semiring (#19581) This PR generalizes Matrix.mul_eq_one_comm from CommRing to CommSemiring.

Estimated changes

added theorem IsUnit.prod_iff
added theorem IsUnit.prod_univ_iff
added theorem IsAddUnit.smul_left
added theorem IsAddUnit.smul_right
modified theorem smulAddHom_apply
added theorem Matrix.isAddUnit_iff
added theorem Equiv.Perm.mem_ofSign
deleted theorem Matrix.mul_eq_one_comm
added def Matrix.adjp
added theorem Matrix.adjp_apply
added def Matrix.detp
added theorem Matrix.detp_mul
added theorem Matrix.detp_one_one
added theorem Matrix.detp_smul_adjp
added theorem Matrix.isAddUnit_mul
added theorem Matrix.mul_eq_one_comm