Documentation Verification Report

Permutation

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

Statistics

Metric	Count
Definitions `permMatrix`, `permMatrixHom`	2
Theorems `conjTranspose_permMatrix`, `det_permutation`, `permMatrixHom_apply`, `permMatrix_l2_opNorm_eq`, `permMatrix_l2_opNorm_le`, `permMatrix_mul`, `permMatrix_mulVec`, `permMatrix_one`, `permMatrix_refl`, `trace_permutation`, `transpose_permMatrix`, `vecMul_permMatrix`	12
Total	14

Equiv.Perm

Definitions

Name	Category	Theorems
`permMatrix` 📖	CompOp	18 math math: `Matrix.transpose_permMatrix`, `Matrix.permMatrix_mem_rowStochastic`, `Matrix.permMatrixHom_apply`, `Matrix.conjTranspose_permMatrix`, `Matrix.permMatrix_mul`, `Matrix.det_permutation`, `Matrix.permMatrix_l2_opNorm_le`, `Matrix.permMatrix_one`, `Matrix.vecMul_permMatrix`, `doublyStochastic_eq_convexHull_permMatrix`, `Matrix.permMatrix_mulVec`, `extremePoints_doublyStochastic`, `Matrix.trace_permutation`, `Matrix.permMatrix_mem_colStochastic`, `permMatrix_mem_doublyStochastic`, `Matrix.permMatrix_refl`, `exists_eq_sum_perm_of_mem_doublyStochastic`, `Matrix.permMatrix_l2_opNorm_eq`

Matrix

Definitions

Name	Category	Theorems
`permMatrixHom` 📖	CompOp	1 math math: `permMatrixHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjTranspose_permMatrix` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Equiv.Perm` `Equiv.Perm.instInv`	—	`transpose_permMatrix` `ext` `star_zero` `star_one`
`det_permutation` 📖	mathematical	—	`det` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddGroupWithOne.toIntCast` `Units.val` `Int.instMonoid` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `Equiv.Perm.sign`	—	`mul_one` `PEquiv.toMatrix_toPEquiv_mul` `det_permute` `det_one` `mul_one`
`permMatrixHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Matrix` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `instMulOneOfFintypeOfDecidableEqOfAddCommMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MonoidHom.instFunLike` `permMatrixHom` `Equiv.Perm.permMatrix` `Equiv.Perm.instInv` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`permMatrix_l2_opNorm_eq` 📖	mathematical	—	`Norm.norm` `Matrix` `NormedRing.toNorm` `instL2OpNormedRing` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Real` `Real.instOne`	—	`le_antisymm` `permMatrix_l2_opNorm_le` `RingHomInvPair.ids` `mulVec_single` `one_smul` `EuclideanSpace.norm_eq` `Finset.sum_congr` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `norm_zero` `ite_pow` `one_pow` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.sum_ite_eq'` `Real.sqrt_one` `EuclideanSpace.single_apply` `mul_one` `l2_opNorm_mulVec`
`permMatrix_l2_opNorm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Matrix` `NormedRing.toNorm` `instL2OpNormedRing` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Real.instOne`	—	`ContinuousLinearMap.opNorm_le_bound` `fact_one_le_two_ennreal` `RCLike.toCompleteSpace` `Real.instZeroLEOneClass` `permMatrix_mulVec` `EuclideanSpace.norm_eq` `Finset.sum_congr` `Equiv.Perm.sum_comp` `Finset.coe_univ` `one_mul`
`permMatrix_mul` 📖	mathematical	—	`Equiv.Perm.permMatrix` `Equiv.Perm` `Equiv.Perm.instMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Equiv.Perm.permMatrix.eq_1` `Equiv.Perm.mul_def` `Equiv.toPEquiv_trans` `PEquiv.toMatrix_trans`
`permMatrix_mulVec` 📖	mathematical	—	`mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`mulVec_eq_sum` `Finset.sum_congr` `PEquiv.transpose_toMatrix_toPEquiv_apply` `IsCentralScalar.op_smul_eq_smul` `Pi.isCentralScalar` `CommSemigroup.isCentralScalar` `Finset.sum_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`
`permMatrix_one` 📖	mathematical	—	`Equiv.Perm.permMatrix` `Equiv.Perm` `Equiv.Perm.instOne` `Matrix` `one`	—	`permMatrix_refl`
`permMatrix_refl` 📖	mathematical	—	`Equiv.Perm.permMatrix` `Equiv.refl` `Matrix` `one`	—	—
`trace_permutation` 📖	mathematical	—	`trace` `AddCommMonoidWithOne.toAddCommMonoid` `Equiv.Perm.permMatrix` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast` `Set.ncard` `Function.fixedPoints` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Finset.sum_congr` `Finset.sum_boole` `Finset.coe_filter`
`transpose_permMatrix` 📖	mathematical	—	`transpose` `Equiv.Perm.permMatrix` `Equiv.Perm` `Equiv.Perm.instInv`	—	`PEquiv.toMatrix_symm` `Equiv.toPEquiv_symm` `Equiv.Perm.inv_def`
`vecMul_permMatrix` 📖	mathematical	—	`vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Equiv.Perm.permMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`vecMul_eq_sum` `Finset.sum_congr` `PEquiv.toMatrix_toPEquiv_apply` `Finset.sum_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`

---

← Back to Index