Hello + adding list lemmas

Stream: new members

[Ethan Pronovost]

Hello! I'm new to Lean. As part of a personal project, I've written a few more lemmas about properties of lists that weren't already in mathlib (as far as I could tell). They all fit the general description of "some property about combining 2 or more list methods". For example

lemma head'_append {α : Type*} {l₁ l₂ : list α} {x : α} (h : x ∈ l₁.head') :  x ∈ (l₁ ++ l₂).head' := ...

Would these sorts of contributions be welcomed in a PR?

[Anne Baanen]

Welcome! New lemmas that you needed for some project are almost always appreciated, so please make your PR! In fact, I'm not aware of any file where we claim the collection of lemmas is complete and quite a few where the opposite holds.

[Ethan Pronovost]

Cool! Can I request to have write access to non-master branches of the mathlib repository as per the instructions here?

[Johan Commelin]

@Ethan Pronovost what is your github username?

[Ethan Pronovost]

@Johan Commelin EPronovost

[Scott Morrison]

Done!

[Ethan Pronovost]

https://github.com/leanprover-community/mathlib/pull/9873