algebra_map simp to smul

Stream: general

[Yakov Pechersky]

@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]

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

[Yakov Pechersky]

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