new planet Hamel and Terrace

[TentativeConvert]

• Level 01-02: introduce vector notation.
• Level 03: introduce scalar multiplication •.
• Level 04: introduce equivFunOnFinite.
• Level 05: Fin.sum_univ_two. sum of Fin 2.
• Level 06: introduce linear combination.
• Level 07: a computation about linear combination.
• Level 08-09: prove linear independent for two vector.
• Level 10: (mini-boss) prove linear independent for infinite vector (bump function).
• Level 11: induction on finite set Finset.induction_on_min.
• Level 12-13: Finset.min' and Finset.min'_le.
• Level 14: linear independent of step function.

[WenrongZou]

Depends on #159. Done.

[WenrongZou]

I am adding Hint and documentation in this PR. I will let you know when it is ready to review.

[TentativeConvert]

Looks like Finset.sum_apply is a new theorem. I think you need another preliminary level to introduce this.

[WenrongZou]

Finset.sum_apply is a simp lemma. I added to simp_list. Then I think we don't need an additional level to introduce it.

[TentativeConvert]

It's a nice level, but perhaps you're right that it distracts from the main aim here. Pairs + the general case should suffice for an introduction. So you can remove this.

[WenrongZou]

I will find out whether we need we need LinearIndependent.pair_iff. I think Fintype.linearIndependent_iff is enough for all these finite indexed linear independent exercise.

[TentativeConvert]

Overall, I think it's good that you added all those elementary levels at the beginning. Finsupp.equivFunOnFinite is a bit difficult to motivate at the beginning, but I also don't have a better idea than simply brushing over this.

[WenrongZou]

I am also not happy with the Finsupp.equivFunOnFinite. I asked in Zulip sometime ago, see here. One option is to make a notation in game like ![1, 2]₀. But I also feel like this will be quite misleading for beginners.

[TentativeConvert]

With the additional level that I requested for sum_apply, we're again hitting the limit of 15 levels. I natural point to cut off would be after the "mini-boss" with the bump function. That would give a nice and not-too-long planet for linear independence. And I suppose the remaining levels with the step functions could then be moved into another short and "optional" planet on which nothing else depends?