Theorems · Theorem · linear algebra
Matrix.permanent_permute_cols
∀ {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 columns does not change the permanent.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Permanent
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 66 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
- Finset.univproof · cited by 3,473
- Finset.prodproof · cited by 2,356
- Equiv.Permstatement and proof · cited by 1,375
- Matrix.submatrixstatement · cited by 183
- Matrix.permanentstatement · cited by 15
- Function.Bijective.sum_compproof · cited by 8
- Group.mulLeft_bijectiveproof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.permanent_permute_rowsproof · cited by 0