Eric Rodriguez
Eric Rodriguez
i'd be a lot more confortable if it could run some basic things, maybe some sort of `push_neg` (with a `wlog!` switch if you're worried about performance). or at least...
In my opinion, the work is done, let's merge it, but let's remove the todo so that extra work isn't done. (I'm still not convinced that the work is unnecesary,...
No worries, best of luck! I'll try finish the review by then :)
isn't the adj matrix `V × V`? I think this is `V × E`
only slightly less than a year later: #18861! (also #18862 for some misc lemmas). I should be getting this done soon, fingers crossed.
Another one is [Nat.toFinset_factors](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/PrimeFin.html#Nat.toFinset_factors)
Maybe just "lemma" or "def" as special keywords? That should be fine to special-case I guess
I think having to comma-separate them doesn't seem unreasonable!
Just a +1 to say that this would be nice!
Scott, does it prevent the crash?