naming contest

Stream: maths

[Patrick Massot]

I have a basis e and a family of vectors v indexed by the same type as e. How do you call the matrix in basis e of the linear map sending e i to v i? It is the matrix whose columns are the vectors indexed by v written on e

def is_basis.give_me_a_name {ι R M : Type*} [fintype ι] [decidable_eq ι]
  [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι → M) : matrix ι ι R :=
linear_equiv_matrix he he (he.constr v)

[Kenny Lau]

is_basis.to_matrix

[Patrick Massot]

Thanks Kenny, you won the contest!