Try to add an inductive definition of a multivector

[eric-wieser]

Moved from #1, this is easier to look at as a PR.

The payoff of all this is that

parameter v : G₁
--  Addition!
#check ((2 + v) : multivector 1)

gives

2 + ↑v : multivector 1

The concepts of blade, hom_mv, and multivector seem to match the chisholm definitions.
The types here do not enforce that the blade vectors are orthogonal, but I don't know how that would be done.

I'm really not happy with:

• my use of cases a, cases b here - there must be a better way to decompose the objects predictably. Fixed!
• the fact that I can't seem to have the coe operations chain automatically

[eric-wieser]

Presumably this counters the goal of:

doesn't depend on data structures, not even canonical structures