Joseph Myers

maintainer merge

maintainer merge

I think my previous comment (that lemmas should be added that can be used to provide `(hf : (orientation.map (fin 2) f.to_linear_equiv o) = complex.orientation)`, for lemmas with such a...

Being at start of line isn't a very safe test at this stage either, because wrapping takes place later and can move text to start of line that only has...

FIxing test function naming (plus any consequent fixes needed for tests to pass) is definitely salvageable! I was thinking mainly about `.` and `-` as the main cases I saw...

I've revised things as suggested to handle HTML tags automatically instead of having separate configuration options.

Results in mathlib should generally be given in appropriately general form. Ceva's theorem (+ converse, which I'm generally considering together) is essentially an affine result; it should work in any...

It's possible that structuring things like I suggest will mean some of your current lemmas are no longer used in the proof, but it's quite possible that such lemmas (in...

Also note that any PR adding a result from Freek's list should make sure to update `docs/100.yaml`.

I don't know of such a resource. A lot of doing things for the weakest type classes is working out as you go along what the weakest type class some...