Commit 2023-04-07 13:27 f5de9eb9

View on Github →

feat: port Data.Matrix.PEquiv (#3234)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/PEquiv.lean

added theorem PEquiv.equiv_toPEquiv_toMatrix

added theorem PEquiv.matrix_mul_apply

added theorem PEquiv.mul_matrix_apply

added theorem PEquiv.mul_toPEquiv_toMatrix

added theorem PEquiv.single_mul_single

added theorem PEquiv.single_mul_single_of_ne

added theorem PEquiv.single_mul_single_right

added def PEquiv.toMatrix

added theorem PEquiv.toMatrix_apply

added theorem PEquiv.toMatrix_bot

added theorem PEquiv.toMatrix_injective

added theorem PEquiv.toMatrix_refl

added theorem PEquiv.toMatrix_swap

added theorem PEquiv.toMatrix_symm

added theorem PEquiv.toMatrix_trans

added theorem PEquiv.toPEquiv_mul_matrix