Theorems · Theorem · combinatorics
Fin.valEmbedding_apply
∀ {n : ℕ}, ⇑Fin.valEmbedding = Fin.val- Defined in
- Mathlib.Data.Fin.Embedding
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
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.
- DFunLike.coestatement and proof · cited by 62,936
- Function.Embeddingstatement · cited by 988
- Fin.valEmbeddingstatement and proof · cited by 30
Cited by5
Results whose statement or proof uses this declaration.
- Finset.map_valEmbedding_attachFinproof · cited by 10
- LinearMap.singularValues_of_finrank_leproof · cited by 1
- List.exists_pw_disjoint_with_cardproof · cited by 1
- Fin.map_valEmbedding_univproof · cited by 1
- Fin.card_filter_val_ltproof · cited by 1