Zulip Chat Archive

Stream: general

Topic: algebra_map simp to smul

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

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

Yakov Pechersky (Mar 01 2021 at 21:51):


Last updated: Aug 03 2023 at 10:10 UTC