OK lecture 2 is about V, the map from subsets of k[X_1,...,X_n] to subsets of k^n. Formalisation went *much* better than lecture 1: https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2FImperialCollegeLondon%2FM4P33%2Fmaster%2Fsrc%2Faffine_algebraic_set%2FV.lean …
I didn't even assume k was a field ;-)
@johncarlosbaez the doc is like a Rosetta Stone for students wanting to learn Lean.
While the code spends 10+ seconds compiling if you're viewing it in a browser, you can just read the extensive comments at the top.
-
-
Permalink which will always work: https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2FImperialCollegeLondon%2FM4P33%2Ff427bb3057138dc9ca52830f3147d3cec443a85a%2Fsrc%2Faffine_algebraic_set%2FV.lean … (the link in the first tweet is broken now because I added some non-mathlib imports)
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.