Theorems · Theorem · linear algebra
Matrix.permanent_transpose
∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]
(M : Matrix n n R), M.transpose.permanent = M.permanentTransposing a matrix preserves the permanent.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Permanent
- Cited by
- 2 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.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · 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.Permproof · cited by 1,375
- Matrix.transposestatement and proof · cited by 389
- Equiv.symm_apply_applyproof · cited by 320
- Function.Involutive.bijectiveproof · cited by 21
- Fintype.prod_equivproof · cited by 18
- Matrix.permanentstatement · cited by 15
Cited by2
Results whose statement or proof uses this declaration.
- Matrix.permanent_permute_rowsproof · cited by 0
- Matrix.permanent_updateRow_smulproof · cited by 0