Zulip Chat Archive

Stream: maths

Topic: naming contest


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Aug 20 2020 at 19:13):

is_basis.to_matrix

view this post on Zulip Patrick Massot (Aug 21 2020 at 08:50):

Thanks Kenny, you won the contest!


Last updated: May 09 2021 at 10:11 UTC