Sums over product types

Stream: new members

[Yakov Pechersky]

Am I missing something that I can use from Pi lemmas? Or are there lemmas missing about pair types? I'm trying to prove lemmas about higher-dim dot products, and am hitting issues proving the following generalized lemma:

import data.finset

universe u
variables {α : Type u} [add_comm_monoid α]

open_locale big_operators

example {u : Type*} {v : Type*} [fintype u] [fintype v] (f : u × v -> α) :
  ∑ (i : u), ∑ (j : v), f (i, j) = ∑ (p : u × v), f p :=
begin
  rw <-finset.sum_product,
  repeat { rw finset.univ },
  sorry,
end

It's getting into the morass of fintype.elems and finsets.

[Chris Hughes]

This'll probably be refl after rw <- finset.sum_product. I don't think it's in the library already and it should be added.

[Chris Hughes]

It won't be refl actually.

[Chris Hughes]

It is refl

[Yakov Pechersky]

Do you think it should be in mathlib in this forward, or in the backward direction?

[Yakov Pechersky]

It's been my recent experience that there aren't a lot of lemmas that work directly on pair types, so perhaps expanding out the pair into the double sum is the better direction.

[Chris Hughes]

It should be the same direction as finset.sum_product

[Yakov Pechersky]

And where would it go? algebra.big_operators has no lemmas that utilize [fintype \a]. Would it be alright to change the imports to introduce fintype?

[Reid Barton]

Those lemmas are in data.fintype I think

[Yakov Pechersky]

Thanks for that guidance. Using that now-defined lemma, I'm trying to prove the equivalent of fin.sum_univ_succ for pair types, and am running into issues, culminating in getting fin to nat coercion to work. My computer has been crashing on memory with Lean and VSCode, so I've had to limit it's available memory. This prevents me from using library_search, so I'm relying a lot on refine _ suggested by suggest. I'm sure this proof can be cleaned up a lot. But the current issue is the final coercion from nat to fin back to nat. It could also be that this has been proved in a more general way for some \Pi u type, I just don't know how to find it, or how to specialize it for pairs. I'd be happy to develop the more general \Pi version if I better understood how pi_finsets work.

import data.matrix.notation

universe u
variables {α : Type u} [add_comm_monoid α] [has_mul α]

open_locale big_operators

@[simp] lemma sum_prod {u : Type*} {v : Type*} [fintype u] [fintype v] (f : u × v -> α) :
  ∑ (i : u), ∑ (j : v), f (i, j) = ∑ (p : u × v), f p :=
begin
  rw <-finset.sum_product,
  refl
end

example {u : Type*} {n : ℕ} [fintype u] [decidable_eq u] (v : fin n.succ × u -> α) :
   ∑ (p : fin n.succ × u), v p =
   ∑ (i : u), v (0, i) + ∑ (ki : fin n × u), v (nat.succ ki.fst, ki.snd) :=
begin
  rw <-@sum_prod α _ (by apply_instance) (fin n) u _,
  rw finset.sum_comm,
  rw <-finset.sum_add_distrib,
  rw <-sum_prod,
  rw finset.sum_comm,
  simp_rw fin.sum_univ_succ,
  refine congr_arg finset.univ.sum _,
  ext i,
  refine congr_arg ((+) (v (0, i))) _,
  refine congr_arg finset.univ.sum _,
  ext j,
  refine congr_arg v _,
  rw prod.eq_iff_fst_eq_snd_eq,
  split,
  { rw fin.coe_eq_val,
    rw fin.eq_iff_veq,
    rw fin.succ_val,
    cases j,
    rw nat.succ_eq_add_one,
    rw <-fin.coe_eq_val,
    sorry }, -- j_val + 1 = ↑↑(j_val + 1)
  { refl }
end

[Yakov Pechersky]

There might be some cleaner way to do this with finset.prod_image, finset.prod_insert, but I think it would have to be on the pi_finsets

[Johan Commelin]

Currently there are a bunch of lemmas that need both fintype and big_operators in data.finitype.card. I think that's a reasonably bad name. Probably that file should be renamed to data.fintype.big_operators

[Johan Commelin]

Maybe even better: all those lemmas don't belong in data.*

[Johan Commelin]

I'm not sure if they belong in algebra.* either. I think initially the goal was to have algebra.* mean "algebraic hierarchy" and it should only contain the definitions (of groups, rings, what have you) and the most basic lemmas.
So maybe the bigops stuff should all move to group_theory.*

[Yakov Pechersky]

Would it make more sense to PR in a couple of small lemmas still into data.fintype.card, and then rearrange later?

[Yakov Pechersky]

It might be easier to do the rearrangement when a critical mass has formed

[Johan Commelin]

Whatever you want. But a "rename a file PR" could also be done right now

[Yakov Pechersky]

In any case, I'm still struggling on how to prove:

import data.finset
import tactic

example {n : ℕ} (x : fin n) : x.succ = ↑((↑x : fin (n + 1)).succ) :=
begin
  unfold_coes,
  rw fin.eq_iff_veq,
  sorry, -- x.succ.val = x.val.cast.succ.val.cast.val
end

[Yakov Pechersky]

There's some weird diamond going on with val, cast, and succ where I can't eliminate any of them

[Johan Commelin]

In which type is that equality taking place?

[Yakov Pechersky]

As far as I understand, it should be taking place in fin (n + 1)

[Yakov Pechersky]

but since there is no arrow on the left, it's probably in fin n

[Johan Commelin]

So on the rhs you are casting x to fin (n+1), then taking succ, which moves it to fin (n+2) and then casting back?

[Bryan Gin-ge Chen]

(deleted)
Whoops, had my cursor in the wrong place.

[Yakov Pechersky]

I guess it is in nat after the rw fin.eq_iff_veq, but the statement at the top is in fin (n + 1)

[Yakov Pechersky]

I think the right hand side is going to fin n --val--> nat --cast--> fin (n + 1) --succ--> fin (n + 1) --val--> nat --cast--> fin (n + 1)

[Johan Commelin]

Right... if possible, I would try to avoid that :stuck_out_tongue_wink:

[Yakov Pechersky]

Or is it fin n --val--> nat --cast--> fin (n + 1) --succ--> fin (n + 2) --val--> nat --cast--> fin (n + 2)

[Johan Commelin]

It is

fin n --val--> nat --cast--> fin (n + 1) --succ--> fin (n + 2) --val--> nat --cast--> fin (n + 1)

[Johan Commelin]

And the cast from nat to fin (? + 1) is taking i to i % (?+1)

[Johan Commelin]

This proof will be a bit messy, because of all those casts

[Yakov Pechersky]

Well it goes back to the proof I'm trying to show above, that sums broken up over pair types works out. The current sum lemmas are on plain fin types, and I don't understand how to employ the pi_finset to prove about pairs.

[Johan Commelin]

hence, maybe it's easier to take a small step back, and see if you can avoid it all together

[Johan Commelin]

Can you instead use sums over finset.range n?

[Johan Commelin]

There is also finset.product to take the cartesian product of two finsets

[Kevin Buzzard]

I would imagine that any proof which involves some funny map from fin(n+2) to fin(n+1) which is "the right thing for the input you have, but crazy in general" is going to have difficulties, for the same reason that theorems involving natural number subtraction are hard in general, even when the subtraction is "the right subtraction in this situation"

[Kevin Buzzard]

Usually I try to refactor subtractions so instead of a-b which is "ok in this situation" I lose the a variable completely and instead use a new variable c such that a=c+b

[Kevin Buzzard]

Looking at what you did, it seems very natural; I am surprised this has happened! Your original statement looks sensible, how did we end up with the casts?

[Kevin Buzzard]

Aah, I think the statement is bad. It contains example (m : ℕ) (i : fin m) : fin (m+1) := nat.succ i. Maybe i.succ is better?

[Kevin Buzzard]

example {u : Type*} {n : ℕ} [fintype u] [decidable_eq u] (v : fin n.succ × u -> α) :
   ∑ (p : fin n.succ × u), v p =
   ∑ (i : u), v (0, i) + ∑ (ki : fin n × u), v (fin.succ ki.fst, ki.snd) :=
begin
  rw <-@sum_prod α _ (by apply_instance) (fin n) u _,
  rw finset.sum_comm,
  rw <-finset.sum_add_distrib,
  rw <-sum_prod,
  rw finset.sum_comm,
  refine congr_arg finset.univ.sum _,
  ext i,
  simp_rw fin.sum_univ_succ,
  -- it's all over
end

Will this do for you? It's an initial segment of your proof, applied to a different statement.

[Kevin Buzzard]

example (n : ℕ) (i : fin n) : nat.succ i = fin.succ i :=
begin
  unfold_coes,
  cases i,
  simp,
end

This is the glue which relates the proof above to your original statement.

[Kevin Buzzard]

Here's a proof of your original statement. I am still a bit confused by all this. Note that it contains a non-terminal simp.

lemma helper (n : ℕ) (i : fin n) : nat.succ i = fin.succ i :=
begin
  unfold_coes,
  cases i,
  simp,
end


example {u : Type*} {n : ℕ} [fintype u] [decidable_eq u] (v : fin n.succ × u -> α) :
   ∑ (p : fin n.succ × u), v p =
   ∑ (i : u), v (0, i) + ∑ (ki : fin n × u), v (nat.succ ki.fst, ki.snd) :=
begin
  simp_rw helper,
  simp,
  rw <-@sum_prod α _ (by apply_instance) (fin n) u _,
  rw finset.sum_comm,
  rw <-finset.sum_add_distrib,
  rw <-sum_prod,
  rw finset.sum_comm,
  simp_rw fin.sum_univ_succ,
end

[Kevin Buzzard]

There's a coercion from nat to fin (nat.succ m) and this is the poorly-behaved map which involves % in general. Avoiding this is the key.

[Yakov Pechersky]

My actual problem is at the bottom of the mwe below. Thanks for all the insights. I'd love to hear more comments about how to incorporate this general sum result into the more specific dot_product proof. I think what is blocking that incorporation is that simp_rw which can't be moved further up.

import data.fintype.card
import data.matrix.basic

open_locale big_operators

namespace matrix

universe u
variables {α : Type u}

open_locale matrix

section matrix_notation
variables {ι : Type} [fintype ι] [decidable_eq ι]

/-- `vec_cons h t` prepends an entry `h` to a vector `t`.

The inverse functions are `vec_head` and `vec_tail`.
The notation `![a, b, ...]` expands to `vec_cons a (vec_cons b ...)`.
-/
def vec_cons {n : ℕ} (h : ι → α) (t : fin n × ι → α) : fin n.succ × ι → α :=
λ p, match p with
| ⟨⟨0, _⟩, i⟩ := h i
| ⟨⟨nat.succ k, hk⟩, i⟩ := t (⟨k, nat.lt_of_succ_lt_succ hk⟩, i)
end

/-- `vec_head v` gives the first entry of the vector `v` -/
def vec_head {n : ℕ} (v : fin n.succ × ι → α) : ι -> α :=
λ i, v (⟨0, nat.succ_pos'⟩, i)

/-- `vec_tail v` gives a vector consisting of all entries of `v` except the first -/
def vec_tail {n : ℕ} (v : fin n.succ × ι → α) : fin n × ι → α :=
λ p, v ⟨⟨nat.succ p.1, nat.succ_lt_succ p.1.2⟩, p.2⟩

end matrix_notation

variables {n : ℕ} {n' : Type} [fintype n'] [decidable_eq n']
variables {ι : Type} [fintype ι] [decidable_eq ι]

section val

@[simp] lemma cons_val_succ (x : ι -> α) (u : fin n × ι → α) (i : fin n) (ix : ι) :
  (vec_cons x u) (i.succ, ix) = u (i, ix) :=
by { simp [vec_cons], cases i, refl }

end val

/-- A product over the `univ` of a pair type equals to
the double product over the `univ`s of the `fst` and `snd` types. -/
@[to_additive "A sum over the `univ` of a pair type equals to
the double sum over the `univ`s of the `fst` and `snd` types."]
lemma fintype.prod_product_fintype {a : Type*} {β : Type*} {M : Type*} [fintype α] [comm_monoid M] [fintype β] {f : α × β → M} :
  ∏ (x : α × β), f x = ∏ x : α, ∏ y : β, f (x, y) :=
by { rw <-finset.prod_product, refl }

section dot_product

variables [add_comm_monoid α] [has_mul α]

@[simp] lemma cons_dot_product [has_mul α] (x : ι -> α) (v : fin n × ι → α) (w : fin n.succ × ι → α) :
  dot_product (vec_cons x v) w = dot_product x (vec_head w) + dot_product v (vec_tail w) :=
begin
  dsimp only [dot_product, vec_head, vec_tail],
  rw [fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      <-finset.sum_add_distrib],
  refine congr_arg finset.univ.sum _,
  ext i,
  rw fin.sum_univ_succ,
  simp_rw [cons_val_succ],  -- I wish I could move this further up, but simp_rw doesn't work higher
  refine congr_arg ((+) _) _,
  refine congr_arg finset.univ.sum _,
  ext j,
  refine congr_arg ((*) (v (j, i))) _,
  refine congr_arg w _,
  unfold_coes,
  cases j,
  simp [fin.eq_iff_veq, fin.succ_val],
  assumption, assumption, -- this line isn't needed in my actual file because sum_product_fintype is properly imported
end

end dot_product

end matrix

[Kevin Buzzard]

I don't really understand this question -- the code compiles. You don't need all those _s in the rewrite in the last proof; rw will put them in for you.

[Kevin Buzzard]

I don't know anything about big operators, I was just intrigued by the puzzle about succ :-)

[Kevin Buzzard]

Why is fintype.prod_product_fintype not a valid simp lemma? This looks like the sort of proof simp would be really good at.

[Kevin Buzzard]

def vec_cons {n : ℕ} (h : ι → α) (t : fin n × ι → α) : fin n.succ × ι → α
| ⟨⟨0, _⟩, i⟩ := h i
| ⟨⟨nat.succ k, hk⟩, i⟩ := t (⟨k, nat.lt_of_succ_lt_succ hk⟩, i)

[Kevin Buzzard]

I think it's better -- better definitional equalities maybe?

[Kevin Buzzard]

e.g.

@[simp] lemma cons_val_succ (x : ι -> α) (u : fin n × ι → α) (i : fin n) (ix : ι) :
  (vec_cons x u) (i.succ, ix) = u (i, ix) :=
by { cases i, refl }

[Kevin Buzzard]

Does this help you?

[Kevin Buzzard]

@Mario Carneiro why isn't fintype.prod_product_fintype a valid simp lemma? I want simp to be doing the donkey work here, don't I?

[Mario Carneiro]

what's the statement?

[Kevin Buzzard]

@Yakov Pechersky that change to the definition of vec_cons lets me move the simp_rw up. Have I solved your problem?

[Kevin Buzzard]

/-- A product over the `univ` of a pair type equals to
the double product over the `univ`s of the `fst` and `snd` types. -/
@[to_additive "A sum over the `univ` of a pair type equals to
the double sum over the `univ`s of the `fst` and `snd` types."]
lemma fintype.prod_product_fintype {a : Type*} {β : Type*} {M : Type*} [fintype α] [comm_monoid M] [fintype β] {f : α × β → M} :
  ∏ (x : α × β), f x = ∏ x : α, ∏ y : β, f (x, y) :=
by { rw <-finset.prod_product, refl }

[Kevin Buzzard]

Those pis are products not Pi types

[Mario Carneiro]

I don't know about this always being a simp lemma, but you should be able to simp with it

[Kevin Buzzard]

simp [fintype.sum_product_fintype], -> invalid simplification lemma 'matrix.fintype.sum_product_fintype' (use command 'set_option trace.simp_lemmas true' for more details)

[Kevin Buzzard]

[simp_lemmas.invalid] rule derived from 'matrix.fintype.sum_product_fintype' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule

[Kevin Buzzard]

fintype.sum_product_fintype :
  ∀ {α : Type u_1} {a : Type u_2} {β : Type u_3} {M : Type u_4} [_inst_5 : fintype α] [_inst_6 : add_comm_monoid M]
  [_inst_7 : fintype β] {f : α × β → M}, ∑ (x : α × β), f x = ∑ (x : α) (y : β), f (x, y)

[Mario Carneiro]

oh!

[Mario Carneiro]

what's a doing there

[Mario Carneiro]

I'm surprised the unused arguments linter didn't catch this

[Kevin Buzzard]

This is not in mathlib

[Kevin Buzzard]

Thanks! I should have linted!

[Kevin Buzzard]

@Yakov Pechersky there's a typo in your definition of fintype.prod_product_fintype -- an {a : Type*} should be {α : Type*}. This explains the random Type goals you get after the rewrite (the assumption, assumption thing). It can now be made into a simp lemma.

[Kevin Buzzard]

The linter also points out that you have two has_mul instances for cons_dot_product. Put #lint at the bottom of your file and take a look at the output.

[Yakov Pechersky]

Thanks for all the insight! Your suggestions made me think of writing another simp lemma, which now makes these higher-dim dot product proofs pretty nice:

import data.fintype.card
import data.matrix.basic

open_locale big_operators

namespace matrix

universe u
variables {α : Type u}

open_locale matrix

section matrix_notation
variables {ι : Type} [fintype ι] [decidable_eq ι]

/-- `![]` is the vector with no entries. -/
def vec_empty : fin 0 × ι → α
| ⟨k, _⟩ := @fin_zero_elim (λ _, α) k

/-- `vec_cons h t` prepends an entry `h` to a vector `t`.

The inverse functions are `vec_head` and `vec_tail`.
The notation `![a, b, ...]` expands to `vec_cons a (vec_cons b ...)`.
-/
def vec_cons {n : ℕ} (h : ι → α) (t : fin n × ι → α) : fin n.succ × ι → α
| ⟨⟨0, _⟩, i⟩ := h i
| ⟨⟨nat.succ k, hk⟩, i⟩ := t (⟨k, nat.lt_of_succ_lt_succ hk⟩, i)

notation `![` l:(foldr `, ` (h t, vec_cons h t) vec_empty `]`) := l

/-- `vec_head v` gives the first entry of the vector `v` -/
def vec_head {n : ℕ} (v : fin n.succ × ι → α) : ι -> α
| i := v (⟨0, nat.succ_pos'⟩, i)

/-- `vec_tail v` gives a vector consisting of all entries of `v` except the first -/
def vec_tail {n : ℕ} (v : fin n.succ × ι → α) : fin n × ι → α
| ⟨⟨k, hk⟩, i⟩ := v ⟨⟨nat.succ k, nat.succ_lt_succ hk⟩, i⟩

end matrix_notation

variables {n : ℕ} {n' : Type} [fintype n'] [decidable_eq n']
variables {ι : Type} [fintype ι] [decidable_eq ι]

section val

@[simp] lemma cons_val_succ (x : ι -> α) (u : fin n × ι → α) (i : fin n) (ix : ι) :
  (vec_cons x u) (i.succ, ix) = u (i, ix) :=
by { cases i, refl }

@[simp] lemma tail_cons' (u : fin (n + 1) × ι → α) (k : fin n) (ix : ι) :
  vec_tail u (k, ix) = u (k.succ, ix) :=
-- by { ext i, simp [vec_tail], cases i, cases i_fst, { simp [fin.cases], }, rw cons_val_succ'',  }
by { cases k, refl }

end val

section dot_product

/-- A product over the `univ` of a pair type equals to
the double product over the `univ`s of the `fst` and `snd` types. -/
@[to_additive "A sum over the `univ` of a pair type equals to
the double sum over the `univ`s of the `fst` and `snd` types."]
lemma fintype.prod_product_fintype {α : Type*} {β : Type*} {M : Type*} [fintype α] [comm_monoid M] [fintype β] {f : α × β → M} :
  ∏ (x : α × β), f x = ∏ x : α, ∏ y : β, f (x, y) :=
by { rw <-finset.prod_product, refl }

variables [add_comm_monoid α] [has_mul α]

@[simp] lemma cons_dot_product (x : ι -> α) (v : fin n × ι → α) (w : fin n.succ × ι → α) :
  dot_product (vec_cons x v) w = dot_product x (vec_head w) + dot_product v (vec_tail w) :=
begin
  dsimp only [dot_product, vec_head, vec_tail],
  rw [fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      <-finset.sum_add_distrib],
  refine congr_arg finset.univ.sum _,
  ext i,
  simpa [fin.sum_univ_succ],
end

@[simp] lemma dot_product_cons (v : fin n.succ × ι → α) (x : ι -> α) (w : fin n × ι → α) :
  dot_product v (vec_cons x w) = dot_product (vec_head v) x + dot_product (vec_tail v) w :=
begin
  dsimp only [dot_product, vec_head, vec_tail],
  rw [fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      <-finset.sum_add_distrib],
  refine congr_arg finset.univ.sum _,
  ext i,
  simpa [fin.sum_univ_succ],
end

end dot_product

end matrix

[Yakov Pechersky]

Even further golfed:

@[simp] lemma cons_dot_product (x : ι -> α) (v : fin n × ι → α) (w : fin n.succ × ι → α) :
  dot_product (vec_cons x v) w = dot_product x (vec_head w) + dot_product v (vec_tail w) :=
begin
  dsimp only [dot_product, vec_head, vec_tail],
  rw [fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      <-finset.sum_add_distrib],
  simpa only [fin.sum_univ_succ, tail_cons', cons_val_succ]
end

@[simp] lemma dot_product_cons (v : fin n.succ × ι → α) (x : ι -> α) (w : fin n × ι → α) :
  dot_product v (vec_cons x w) = dot_product (vec_head v) x + dot_product (vec_tail v) w :=
begin
  dsimp only [dot_product, vec_head, vec_tail],
  rw [fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      fintype.sum_product_fintype, @finset.sum_comm ι _ _ _ _ _ _,
      <-finset.sum_add_distrib],
  simpa only [fin.sum_univ_succ, tail_cons', cons_val_succ]
end

[Yakov Pechersky]

I'd been banging my head against the wall for like 4-5 days on these lemmas. And turns out just defining the fintype.prod_product_fintype and tail_cons' was all I needed. Is that a normal proof workflow? I feel like I went down too many wrong paths.

[Patrick Massot]

I haven't been following the discussion but the last message sounds like you're learning.

[Patrick Massot]

Without having any idea about the topic of the discussion, I can see uncurried functions and lots of underscores. This doesn't smell good.

[Yakov Pechersky]

The uncurried functions are due to my trying to make lemmas about higher-dim "matrices" without having to rewrite them for b -> a, c -> b -> a, d -> c -> b -> a.

[Yakov Pechersky]

where the head of those arguments is always a fin n. So my proving over the product type, I can stuff the rest of the arrows all into the \io index type.

[Patrick Massot]

This is fishy.

[Patrick Massot]

What do you call higher-dim matrices? Tensors?

[Kevin Buzzard]

Yakov yes, this is exactly the workflow for learning Lean. You get interested in something, you work on it, you come up with some concrete Lean code which works, or doesn't quite work, you post it, others look at it and suggest fixes or changes, and proofs just get neater and neater. It doesn't matter how much you understand the material "informally", there is some kind of a knack for getting it into Lean which you learn by doing (writing code) and getting others to look at it. The vast majority of us learnt this way. The power of this chat is that there are a whole bunch of experts on it -- your situation was sufficiently basic that an intermediate user like me could help, but as you get better and maybe more specialised then you ask more challenging questions with your code and experts who know the system inside out give you more subtle answers (e.g. there are very subtle questions which can come up regarding e.g. the type class inference system).

[Yakov Pechersky]

I'm a fan of that sort of learning style. The hope is that everyone remains eager to teach each other

[Yakov Pechersky]

What do you find fishy about that sort of construction, Patrick?

[Yakov Pechersky]

Once could call them tensors, although in a mathlib that seems inappropriate. Higher dim matrices is a numpy style moniker.

[Kevin Buzzard]

I thought they were called holors :-)

[Yakov Pechersky]

Holors, from what I looked at in the lib, don't have good support for cons, they seemed to me to be more about construct-once at desired shape

[Yakov Pechersky]

I'm editing the matrix notation file, and didn't want to write repetitive lemmas about matrices for the ones that were already written about vectors. Seemed to me that they were general statements about cons, head, tail, etc that did not rely on 1- or 2- dimensionality

[Yakov Pechersky]

And also a good way to flex/train my lean programming skills