Nat.nsmul_eq_mul

theorem Nat.nsmul_eq_mul : ∀ (m n : ℕ), m • n = m * n

This theorem states that for any two natural numbers `m` and `n`, the scalar multiplication `m • n` is equal to the regular multiplication `m * n`. In simpler terms, multiplying `n` by `m` times is the same as just multiplying `m` and `n`.

More concisely: For all natural numbers m and n, m • n = m * n. (Scalar multiplication equals regular multiplication for natural numbers.)