semiring nsmul

Stream: Is there code for X?

[Kim Morrison]

Surely this already has a name somewhere?

import Mathlib

example {α} [Semiring α] (n : ℕ) (a : α) : n • a = (n : α) * a := by
  induction n with
  | zero => simp [zero_nsmul]
  | succ n ih =>
    simp [succ_nsmul, ih, right_distrib]

[Aaron Liu]

Probably something like docs#nsmul_eq_mul

[Kim Morrison]

ah, I didn't actually have that imported!