Theorems · Theorem · linear algebra
Matrix.permanent_permute_rows
∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (σ : Equiv.Perm n)
(M : Matrix n n R), (M.submatrix id ⇑σ).permanent = M.permanentPermuting the rows does not change the permanent.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Permanent
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommSemiringstatement and proof · cited by 10,911
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- Equiv.Permstatement and proof · cited by 1,375
- Matrix.transposeproof · cited by 389
- Matrix.submatrixstatement and proof · cited by 183
- Matrix.permanentstatement and proof · cited by 15
- Matrix.transpose_submatrixproof · cited by 12
- Matrix.permanent_transposeproof · cited by 2
- Matrix.permanent_permute_colsproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.