Zulip Chat Archive

Stream: general

Topic: naming contest


view this post on Zulip Anne Baanen (Oct 16 2020 at 15:11):

Any suggestions for a conciser name?

lemma is_basis_to_matrix_mul_linear_map_to_matrix_mul_is_basis_to_matrix
  (hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
  hc.to_matrix c'  linear_map.to_matrix hb' hc' f  hb'.to_matrix b = linear_map.to_matrix hb hc f := sorry

view this post on Zulip Eric Wieser (Oct 16 2020 at 15:24):

Can that be split into two lemmas?

lemma is_basis_to_matrix_mul_linear_map_to_matrix
  (hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
  hc.to_matrix c'  linear_map.to_matrix hb' hc' f = linear_map.to_matrix hb' hc f := sorry

and a similar linear_map_to_matrix_mul_is_basis_to_matrix?

Or am I missing something there?

view this post on Zulip Anne Baanen (Oct 16 2020 at 15:26):

Ah good point, I was thinking about how to describe "basis change" in Lean.

view this post on Zulip Anne Baanen (Oct 16 2020 at 15:26):

But we can do it one side at a time.

view this post on Zulip Anne Baanen (Oct 16 2020 at 15:27):

Still quite a long name :/

view this post on Zulip Gabriel Ebner (Oct 16 2020 at 16:09):

You could turn one of the underscores into a dot and put it in the is_basis namespace.

view this post on Zulip Gabriel Ebner (Oct 16 2020 at 16:10):

Eric's version also looks like a good simp lemma.


Last updated: May 13 2021 at 00:41 UTC