Zulip Chat Archive

Stream: general

Topic: algebra_map simp to smul


view this post on Zulip Yakov Pechersky (Mar 01 2021 at 21:45):

@Eric Wieser asked on #6496, should algebra_map's simp-normal form be the smul, like in the lemma I am PRing?

@[simp] lemma matrix.algebra_map_eq_smul (n : Type u) {R : Type v} [decidable_eq n] [fintype n]
  [comm_semiring R] (r : R) : (algebra_map R (matrix n n R)) r = r  1 := rfl

view this post on Zulip Eric Wieser (Mar 01 2021 at 21:49):

There's a thread somewhere suggesting the normal form be coe r instead, it might be worth linking that

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 21:51):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20.60algebra_map.60.20.2F.20.60algebra.2Eof_id.60


Last updated: May 11 2021 at 22:14 UTC