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.
-
Prikaži ovu nit
-
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.
1 reply 0 proslijeđenih tweetova 0 korisnika označava da im se sviđaPrikaži ovu nit
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)
04:36 - 18. sij 2020.
0 replies
1 proslijeđeni tweet
1 korisnik označava da mu se sviđa
Č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.