Commit 2025-01-27 14:13 12422efb

chore(Data/Matrix/PEquiv): clean up names (#21108) This renames and deprecates:

• PEquiv.mul_matrix_apply -> PEquiv.toMatrix_mul_apply
• PEquiv.matrix_mul_apply -> PEquiv.mul_toMatrix_apply
• PEquiv.toPEquiv_mul_matrix -> PEquiv.toMatrix_toPEquiv_mul
• PEquiv.mul_toPEquiv_toMatrix -> PEquiv.mul_toMatrix_toPEquiv
• PEquiv.equiv_toPEquiv_toMatrix -> PEquiv.toMatrix_toPEquiv_eq Also adds two more convenience lemmas, and removes an unused classical tactic.