Swap

📁 Source: Mathlib/LinearAlgebra/Matrix/Swap.lean

Statistics

Metric	Count
Definitions swap, swap	2
Theorems map_swap, val_inv_swap, val_swap, conjTranspose_swap, map_swap, mul_swap_apply_left, mul_swap_apply_right, mul_swap_of_ne, swap_comm, swap_mulVec, swap_mulVec_apply, swap_mul_apply_left, swap_mul_apply_right, swap_mul_of_ne, swap_mul_self, transpose_swap, vecMul_swap, vecMul_swap_apply	18
Total	20

Matrix

Definitions

Name	Category	Theorems
swap 📖	CompOp	17 math math: swap_mul_self, map_swap, swap_mulVec_apply, conjTranspose_swap, swap_mul_apply_right, mul_swap_of_ne, mul_swap_apply_left, swap_mulVec, swap_mul_of_ne, transpose_swap, GeneralLinearGroup.val_swap, vecMul_swap_apply, swap_mul_apply_left, GeneralLinearGroup.val_inv_swap, swap_comm, mul_swap_apply_right, vecMul_swap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjTranspose_swap 📖	mathematical	—	conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	conjTranspose_permMatrix
map_swap 📖	mathematical	—	map swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom RingHom.instFunLike	—	PEquiv.map_toMatrix
mul_swap_apply_left 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.mul_toMatrix_toPEquiv Equiv.swap_apply_left
mul_swap_apply_right 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	swap_comm mul_swap_apply_left
mul_swap_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.mul_toMatrix_toPEquiv Equiv.swap_apply_of_ne_of_ne
swap_comm 📖	mathematical	—	swap	—	Equiv.swap_comm
swap_mulVec 📖	mathematical	—	mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap	—	PEquiv.toMatrix_toPEquiv_mulVec
swap_mulVec_apply 📖	mathematical	—	mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.toMatrix_toPEquiv_mulVec Equiv.swap_apply_left
swap_mul_apply_left 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.toMatrix_toPEquiv_mul Equiv.swap_apply_left
swap_mul_apply_right 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	swap_comm swap_mul_apply_left
swap_mul_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.toMatrix_toPEquiv_mul Equiv.swap_apply_of_ne_of_ne
swap_mul_self 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne one	—	Equiv.swap_inv Equiv.Perm.inv_def Equiv.swap_swap PEquiv.toMatrix_refl
transpose_swap 📖	mathematical	—	transpose swap	—	transpose_permMatrix
vecMul_swap 📖	mathematical	—	vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap	—	PEquiv.vecMul_toMatrix_toPEquiv
vecMul_swap_apply 📖	mathematical	—	vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	PEquiv.vecMul_toMatrix_toPEquiv Equiv.swap_apply_left

Matrix.GeneralLinearGroup

Definitions

Name	Category	Theorems
swap 📖	CompOp	3 math math: map_swap, val_swap, val_inv_swap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_swap 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike map swap	—	Units.ext Matrix.map_swap
val_inv_swap 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv swap Matrix.swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
val_swap 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring swap Matrix.swap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—

---

← Back to Index