Kevin Buzzard

### Prerequisites * [X ] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues)....

feat(Tactic/ByContra): by_contra' tactic

3

Implementation of `by_contra'`. Note that it needs the (as yet unimplemented) `push_neg`.

variable H bug with `∀ h ∈ H`

2

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

put link to html version of book in README

1

I know I'm an idiot who can't use the internet, but search for me stubbornly refuses to give me the URL of the web-based version of this book. I'm always...

do example of norm_cast

Tidy up this repo

2

Tidy up the project. Ideas: 1) Imperial subdirectory with dirs M1F, M2PM2 etc where we prove theorems in current courses. 2) Library xenalib, I want to put e.g. Keji's det(A)det(B)...

This is basically a note to myself. I just looked at the current issue of Annals of Mathematics (one of the top, if not the top, pure maths journal) to...

Structure presheaf on an affine scheme is a sheaf

8

What is left: 1) Sheaf axiom for finite cover of Spec(R) by opens of the form D(f). 2) Sheaf axiom for finite cover by opens D(f) implies sheaf axiom for...

Maps from a scheme to an affine scheme Spec(R) are the same as maps from R to the global sections of the scheme. This result, which extends to locally ringed...

disappearing text in tutorial world entry page

2

This has taken a while to pin down, and now I've pinned it down I don't have any understanding of what's going on. The comments below pertain to the `debug`...