Theorems · Definition · linear algebra
Equiv.Perm.permMatrix
{n : Type u_1} → (R : Type u_2) → [DecidableEq n] → Equiv.Perm n → [Zero R] → [One R] → Matrix n n Rthe permutation matrix associated with an Equiv.Perm
- Defined in
- Mathlib.LinearAlgebra.Matrix.Permutation
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqZeroOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrixstatement · cited by 4,303
- Equiv.Permstatement and proof · cited by 1,375
- PEquiv.toMatrixproof · cited by 25
- Equiv.toPEquivproof · cited by 23
Cited by27
Results whose statement or proof uses this declaration.
- Matrix.swapproof · cited by 19
- Matrix.transpose_permMatrixstatement and proof · cited by 2
- Matrix.permMatrix_l2_opNorm_lestatement and proof · cited by 2
- Matrix.swap_commproof · cited by 2
- doublyStochastic_eq_convexHull_permMatrixstatement and proof · cited by 2
- permMatrix_mem_doublyStochasticstatement · cited by 2
- Matrix.transpose_swapproof · cited by 1
- Matrix.conjTranspose_permMatrixstatement and proof · cited by 1
- Matrix.permMatrixHomproof · cited by 1
- Matrix.permMatrix_mulVecstatement and proof · cited by 1
- Matrix.permMatrix_reflstatement · cited by 1
- exists_eq_sum_perm_of_mem_doublyStochasticstatement and proof · cited by 1