Theorems · Theorem · linear algebra
Pi.basisFun_repr
∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η] (x : η → R) (i : η), ((Pi.basisFun R η).repr x) i = x i
- Defined in
- Mathlib.LinearAlgebra.StdBasis
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 77 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 · cited by 62,936
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- Finsuppstatement · cited by 5,255
- LinearEquivstatement · cited by 3,317
- Finitestatement and proof · cited by 3,029
- Module.Basis.reprstatement · cited by 498
- Pi.basisFunstatement · cited by 78
Cited by11
Results whose statement or proof uses this declaration.
- LinearMap.toMatrix₂'_compl₁₂proof · cited by 6
- ZLattice.covolume.tendsto_card_div_pow''proof · cited by 2
- ZLattice.covolume.tendsto_card_le_div''proof · cited by 2
- BoxIntegral.unitPartition.mem_smul_span_iffproof · cited by 2
- NumberField.mixedEmbedding.fundamentalDomain_stdBasisproof · cited by 1
- ZSpan.fundamentalDomain_pi_basisFunproof · cited by 1
- Matrix.toBilin_basisFunproof · cited by 0
- Pi.mem_spanSubset_iffproof · cited by 0
- Matrix.toLinearMap₂_basisFunproof · cited by 0
- LDL.lowerInv_triangularproof · cited by 0