Theorems · Theorem · linear algebra
LinearMap.toMatrix_singleton
∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_7} [inst_1 : Unique ι] (f : R →ₗ[R] R) (i j : ι),
(LinearMap.toMatrix (Module.Basis.singleton ι R) (Module.Basis.singleton ι R)) f i j = f 1- Defined in
- Mathlib.LinearAlgebra.Matrix.ToLin
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringUnique
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
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
- RingHom.idstatement and proof · cited by 18,349
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement and proof · cited by 10,215
- Matrixstatement · cited by 4,303
- mul_oneproof · cited by 3,885
- LinearEquivstatement · cited by 3,317
- Finset.sum_congrproof · cited by 2,323
- Pi.singleproof · cited by 518
- Uniquestatement and proof · cited by 400
- LinearEquiv.transproof · cited by 298
- LinearMap.toMatrixstatement · cited by 180
Cited by1
Results whose statement or proof uses this declaration.
- LinearMap.det_ringproof · cited by 9