Theorems · Inductive type · linear algebra
Matrix.TransvectionStruct
Type u_1 → Type u₂ → Type (max u_1 u₂)
A structure containing all the information from which one can build a nontrivial transvection. This structure is easier to manipulate than transvections as one has a direct access to all the relevant fields.
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by56
Results whose statement or proof uses this declaration.
- Matrix.TransvectionStruct.toMatrixstatement and proof · cited by 32
- Matrix.TransvectionStruct.invstatement and proof · cited by 11
- Matrix.TransvectionStruct.istatement and proof · cited by 7
- Matrix.TransvectionStruct.casesOnstatement and proof · cited by 6
- Matrix.TransvectionStruct.jstatement and proof · cited by 6
- Matrix.TransvectionStruct.toSpecialLinearGroupstatement and proof · cited by 6
- Matrix.TransvectionStruct.cstatement and proof · cited by 5
- Matrix.TransvectionStruct.detstatement and proof · cited by 4
- Matrix.TransvectionStruct.hijstatement and proof · cited by 4
- Matrix.TransvectionStruct.sumInlstatement and proof · cited by 4
- Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvecstatement and proof · cited by 3
- Matrix.TransvectionStruct.reindexEquivstatement and proof · cited by 3