Theorems · Theorem
Matrix.Fin.snoc_vecCons
∀ {n : ℕ} {α : Type u_1} (x y : α) (p : Fin n → α), Fin.snoc (Matrix.vecCons y p) x = Matrix.vecCons y (Fin.snoc p x)We push Fin.snoc inside vecCons. This allows us to simplify e.g.
Fin.snoc ![1, 3, 7] 5 to ![1, 3, 7, 5].
- Defined in
- Mathlib.Data.Fin.VecNotation
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
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.
- Matrix.vecConsstatement · cited by 852
- Fin.snocstatement · cited by 113
- Fin.cons_snoc_eq_snoc_consproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- exists_linearIndependent_pair_of_one_lt_rankproof · cited by 2