Data.Finsupp.Basic !4#1949

Stream: mathlib4

[Jireh Loreaux]

I took a decent swing at this, but it's not done yet. I'm going to teach and eat dinner, so I won't be able to work on it for a few hours. So if anyone wants to give it a shot, that's fine, just post here. I'll come back to this later tonight.

[Jireh Loreaux]

!4#1949 is now ready for review. This should let us unlock more linear algebra. @Floris van Doorn : am I correct in assuming the issue with simps is not yet fixed?

I have to step away until tomorrow, so I won't be able to make updates based on code review, so if anyone wants to do so, go for it.

[Floris van Doorn]

The issue with noncomputable section is lean4#2077 and is indeed not yet fixed. However, after !4#1958 I don't think it affects simps anymore. Note that it still affects definitions marked as simp (without s). If you (redundantly) add noncomputable in front of every definition that has the simp attribute (if any), I think the attribute will be added (see example in lean4#2077)