Theorems · Theorem · linear algebra
Pi.basisFun_apply
∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η] [inst_2 : DecidableEq η] (i : η), (Pi.basisFun R η) i = Pi.single i 1
- Defined in
- Mathlib.LinearAlgebra.StdBasis
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringFiniteDecidableEq
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 · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Finitestatement and proof · cited by 3,029
- Module.Basisstatement · cited by 1,477
- Pi.singlestatement and proof · cited by 518
- LinearEquiv.reflproof · cited by 143
- Pi.basisFunstatement · cited by 78
- Module.Basis.coe_ofEquivFunproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- LinearMap.toMatrix₂'_compl₁₂proof · cited by 6
- Matrix.stdBasis_eq_singleproof · cited by 3
- Algebra.PreSubmersivePresentation.aevalDifferential_singleproof · cited by 3
- Matrix.rank_eq_finrank_range_toLinproof · cited by 2
- Algebra.SubmersivePresentation.basisDeriv_applyproof · cited by 2
- TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegularproof · cited by 1
- LinearMap.toLinearMap₂'Aux_toMatrix₂Auxproof · cited by 1
- AlgHom.eq_piEvalAlgHomproof · cited by 1
- basis_toMatrix_basisFun_mulproof · cited by 1
- LinearMap.toMatrix₂_basisFunproof · cited by 1