## Stream: maths

### Topic: naming contest

#### Patrick Massot (Aug 20 2020 at 19:11):

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 (Aug 20 2020 at 19:13):

is_basis.to_matrix

#### Patrick Massot (Aug 21 2020 at 08:50):

Thanks Kenny, you won the contest!

Last updated: May 09 2021 at 10:11 UTC