Theorems · Theorem · combinatorics
Fin.append_left_eq_cons
∀ {α : Sort u_1} {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α), Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast ⋯Appending a one-tuple to the left is the same as Fin.cons.
- Defined in
- Mathlib.Data.Fin.Tuple.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fin.consstatement and proof · cited by 190
- Fin.cons_succproof · cited by 54
- Fin.cons_zeroproof · cited by 53
- Fin.appendstatement and proof · cited by 50
- Fin.append_leftproof · cited by 17
- Fin.append_rightproof · cited by 16
Cited by3
Results whose statement or proof uses this declaration.
- TensorPower.list_prod_gradedMonoid_mk_singleproof · cited by 1
- Fin.append_left_snocproof · cited by 1
- Fin.cons_eq_appendproof · cited by 0