mathlib3

e77f071c - feat(linear_algebra/{clifford,exterior,tensor}_algebra): add induction principles (#6416)

feat(linear_algebra/{clifford,exterior,tensor}_algebra): add induction principles (#6416) These are closely derived from the induction principle for the free algebra. I can't think of a good way to deduplicate them, so for now I've added comments making it clear to the reader that the code is largely copied.