Theorems · Definition · combinatorics
Composition.index
{n : ℕ} → (c : Composition n) → Fin n → Fin c.lengthc.index j is the index of the block in the composition c containing j.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.findproof · cited by 139
- Compositionstatement and proof · cited by 138
- Composition.lengthstatement · cited by 92
Cited by11
Results whose statement or proof uses this declaration.
- Composition.invEmbeddingstatement and proof · cited by 5
- Composition.blocksFinEquivproof · cited by 3
- Composition.embedding_comp_invstatement · cited by 2
- Composition.mem_range_embedding_iff'statement and proof · cited by 2
- Composition.sizeUpTo_index_lestatement and proof · cited by 1
- Composition.index_embeddingstatement · cited by 1
- Composition.mem_range_embeddingstatement and proof · cited by 1
- Composition.invEmbedding_compstatement · cited by 0
- Composition.lt_sizeUpTo_index_succstatement · cited by 0
- FormalMultilinearSeries.applyComposition_updatestatement and proof · cited by 0
- Composition.coe_invEmbeddingstatement · cited by 0