Theorems · Definition · linear algebra
Holor
Type u → List ℕ → Type u
Holor (indexed collections of tensor coefficients)
- Defined in
- Mathlib.Data.Holor
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- HolorIndexproof · cited by 16
Cited by40
Results whose statement or proof uses this declaration.
- Holor.mulstatement and proof · cited by 10
- Holor.CPRankMaxstatement · cited by 8
- Holor.slicestatement and proof · cited by 7
- Holor.CPRankMax1statement · cited by 5
- Holor.CPRankMax.belowstatement · cited by 3
- Holor.CPRankMax.brecOnstatement and proof · cited by 2
- Holor.cprankMax_addstatement and proof · cited by 2
- Holor.unitVecstatement · cited by 2
- Holor.assocLeftstatement · cited by 1
- Holor.cast_typestatement and proof · cited by 1
- Holor.cprankstatement and proof · cited by 1
- Holor.cprankMax_1statement and proof · cited by 1