Mapping a function over ![…] #
[UPSTREAM] candidate for Mathlib/Data/Fin/VecNotation.lean. The η-expanded
forms of Fin.comp_cons and of the empty case, stated on the lambda
fun i => f (![a, …] i) so that simp pushes f into a vector literal.
theorem
Matrix.comp_vecCons
{α : Type u_1}
{β : Type u_2}
{n : ℕ}
(f : α → β)
(a : α)
(v : Fin n → α)
:
(fun (i : Fin n.succ) => f (vecCons a v i)) = vecCons (f a) fun (i : Fin n) => f (v i)
theorem
Matrix.comp_vecEmpty
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
(fun (i : Fin 0) => f (![] i)) = ![]