Multiply an Alpha type with a natural type.

Stream: new members

[Colin Jones ⚛️]

Hi all,

I was wondering if it was possible to easily set up the second definition summa_mul to work out. In the second definition, I need help adding an instance to allow for the multiplication of an alpha and a natural number. Is this possible? And, if so, how can I do this?

import Mathlib

open BigOperators Filter Finset Nat Set

variable (n m : ℕ) (w z : ℤ) (p q : ℚ) (x y : ℝ) (a b : α)

def summa (a : α) [AddCommMonoid α] : α := ∑ i in range n, a

def summa_mul (a : α) [AddCommMonoid α] [HMul α ℕ] : α := ∑ i in range n, a*i
-- Here is the error!

#eval summa 5 (8/9 : ℚ)

#eval summa 8 (1/2 : ℚ)

[Kevin Buzzard]

docs#HMul takes three inputs: if you feed it X, Y and Z, then this means that x * y : Z if x : X and y : Y. So if you want the type of a * i to be alpha again, then you want [HMul α ℕ α].

[Eric Wieser]

Usually we would write this

def summa_mul (a : α) [AddCommMonoid α] : α := ∑ i in range n, i • a

[Eric Wieser]

Here • is "the obvious multiplication by the naturals" not just "some arbitrary function that is written with a * symbol