Commit 2025-02-18 09:18 99a0bc08

View on Github →

feat(LinearAlgebra/Matrix): swap matrices (#19812) We define and establish basic API for swap matrices. Matrix.swap R i j is the matrix that, when multiplying on the left, swaps the i-th and j-th row. From "Formalizing the Bruhat-Tits tree"

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

added theorem Pi.mulSingle_comp_equiv

Modified Mathlib/LinearAlgebra/Matrix/Permutation.lean

added theorem Matrix.conjTranspose_permMatrix

added theorem Matrix.transpose_permMatrix

Created Mathlib/LinearAlgebra/Matrix/Swap.lean

added theorem Matrix.GeneralLinearGroup.map_swap

added def Matrix.GeneralLinearGroup.swap

added theorem Matrix.conjTranspose_swap

added theorem Matrix.map_swap

added theorem Matrix.mul_swap_apply_left

added theorem Matrix.mul_swap_apply_right

added theorem Matrix.mul_swap_of_ne

added def Matrix.swap

added theorem Matrix.swap_comm

added theorem Matrix.swap_mulVec

added theorem Matrix.swap_mulVec_apply

added theorem Matrix.swap_mul_apply_left

added theorem Matrix.swap_mul_apply_right

added theorem Matrix.swap_mul_of_ne

added theorem Matrix.swap_mul_self

added theorem Matrix.transpose_swap

added theorem Matrix.vecMul_swap

added theorem Matrix.vecMul_swap_apply