Theorems · Definition · combinatorics
Composition.embedding
{n : ℕ} → (c : Composition n) → (i : Fin c.length) → Fin (c.blocksFun i) ↪o Fin nEmbedding the i-th block of a composition (identified with Fin (c.blocksFun i)) into
Fin n at the relevant position.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 27 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.
- OrderEmbeddingstatement · cited by 619
- Compositionstatement and proof · cited by 138
- Composition.lengthstatement and proof · cited by 92
- Composition.blocksFunstatement · cited by 52
- RelEmbedding.transproof · cited by 27
- Composition.sizeUpToproof · cited by 26
- Fin.castLEOrderEmbproof · cited by 4
- Fin.natAddOrderEmbproof · cited by 3
Cited by27
Results whose statement or proof uses this declaration.
- FormalMultilinearSeries.applyCompositionproof · cited by 24
- Composition.blocksFinEquivproof · cited by 3
- FormalMultilinearSeries.applyComposition_onesproof · cited by 3
- Composition.embedding_comp_invstatement · cited by 2
- Composition.mem_range_embedding_iff'statement and proof · cited by 2
- FormalMultilinearSeries.compContinuousLinearMap_applyCompositionproof · cited by 2
- FormalMultilinearSeries.comp_partialSumproof · cited by 2
- FormalMultilinearSeries.comp_rightInv_aux2proof · cited by 2
- Composition.single_embeddingstatement · cited by 2
- FormalMultilinearSeries.removeZero_applyCompositionproof · cited by 2
- Composition.disjoint_rangestatement and proof · cited by 1
- Composition.index_embeddingstatement · cited by 1