Kyle Miller

I think it would be good to split off a new PR of just the stuff about unoriented incidence matrices. Things about orientations and oriented incidence matrices can wait in...

@dimpase I get that (and I very much want that factorization of the Laplacian matrix) -- what I've been thinking is that orientations should probably come from `simple_digraph`, which doesn't...

It might also be OK for orientations to be their own thing. I'd suggest changing the definition, though, to something that is closer to the definition of `simple_graph`. Here's a...

@Kha What do you think about this implementation? Do you have any ideas how to make it not parenthesize atomic syntax? In particular, is there some condition that implies parentheses...

@Kha I've tried a few variations on that, but they didn't seem to have any effect. I think I've spent my time budget on this feature -- maybe if it...

Many of the proofs are monstrosities right now. It seems like there are patterns in proofs that could be turned into lemmas, but I was just focused on getting the...

@barrettj12 Thanks. I think what can be helpful at this point is to figure out how to simplify the proofs of the things starting around line 1000 of connectivity.lean. There...

Sebastian and I were discussing this today, and I had a few thoughts and concerns that he thought I should document here: - Sometimes string literals appear in syntactic locations...