Theorems · Theorem
Matrix.cons_val_succ
∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) (i : Fin m), Matrix.vecCons x u i.succ = u i- Defined in
- Mathlib.Data.Fin.VecNotation
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrix.vecConsstatement · cited by 852
- Fin.cons_succproof · cited by 54
Cited by47
Results whose statement or proof uses this declaration.
- Matrix.cons_val'proof · cited by 88
- Matrix.tail_consproof · cited by 16
- WeierstrassCurve.Projective.smul_fin3proof · cited by 14
- Matrix.range_consproof · cited by 14
- Matrix.smul_consproof · cited by 9
- Matrix.cons_mulproof · cited by 8
- Matrix.neg_consproof · cited by 6
- FirstOrder.Language.BoundedFormula.realize_rel₂proof · cited by 6
- Orientation.eq_or_eq_neg_of_isEmptyproof · cited by 6
- Matrix.dotProduct_consproof · cited by 5
- Matrix.add_consproof · cited by 5
- liftFun_vecConsproof · cited by 4