vector_map_id missing?

Stream: new members

[Vaibhav Karve]

Is this missing from mathlib? I wanted to use this in one of my proofs but had to prove it by hand because library_search and suggest told me it is not already in mathlib. Is that correct? Does it need to be added in?

lemma vec_map_id {α : Type} {n : ℕ} (v : vector α n) : vector.map id v = v :=
begin
  induction n,
    {simp only [eq_iff_true_of_subsingleton]},
  cases v with vl vn,
  unfold vector.map,
  norm_num,
end

[Scott Morrison]

I'm not seeing it either. I suspect there's a nicer proof in terms of .to_list.

[Yakov Pechersky]

import data.vector2

lemma vector.map_id {α : Type} {n : ℕ} (v : vector α n) : vector.map id v = v :=
begin
  apply vector.eq,
  simp only [list.map_id, vector.to_list_map]
end

[Filippo A. E. Nuccio]

Isn't it linear_map.id in linear_algebra.basic?

[Anne Baanen]

This is a computer science vector, i.e. a list with fixed length :)

[Eric Wieser]

This is worth a quick PR, right?

[Anne Baanen]

Quick PRs are always worth the effort!

[Eric Wieser]

Presumably the proof golfs to vector.eq (by simp)?

[Vaibhav Karve]

Almost. I think it's vector.eq _ _ (by simp).

[Vaibhav Karve]

@Eric Wieser if you don't mind, can I create the PR? I have never contributed to mathlib before and I would like to learn :-)

[Vaibhav Karve]

@maintainers Can I get write access for the non-master branches of mathlib? Github username: vaibhavkarve. Thank you for your time!

[Mario Carneiro]

invitation sent

[Vaibhav Karve]

I opened a PR here: https://github.com/leanprover-community/mathlib/pull/4799

[Yury G. Kudryashov]

#4799 works too