Theorems · Theorem · linear algebra
PEquiv.transpose_toMatrix_toPEquiv_apply
∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
[inst_3 : One α] (f : m ≃ n) (j : n), f.toPEquiv.toMatrix.transpose j = Pi.single (f.symm j) 1- Defined in
- Mathlib.Data.Matrix.PEquiv
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Equivstatement and proof · cited by 8,337
- Equiv.symmstatement and proof · cited by 3,681
- Pi.singlestatement · cited by 518
- Matrix.transposestatement · cited by 389
- Pi.single_applyproof · cited by 78
- PEquiv.toMatrixstatement · cited by 25
- Equiv.toPEquivstatement and proof · cited by 23
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.permMatrix_mulVecproof · cited by 1