## 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):

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