lean-liquid
lean-liquid copied to clipboard
leanprover-community
💧 Liquid Tensor Experiment
This PR does a couple of things. 1) I remove all irrelevant imports, opens and open-locales. Undocumented and unused commands just confuse the non-expert reader. 2) I write the document...
I've added a lot of comments for the `profinite` example Lean file. My personal opinion from having watched students is that there are two kinds. There are those that don't...
If `𝒜` is a concrete monoidal abelian category, show that sheaves with values in `𝒜` also form a monoidal abelian category. Prove the tensor-hom adjunction. In fact, we only need...
Oh no! We have failed to automatically upgrade your project to the latest versions of Lean and its dependencies. If your project currently builds, this is probably because of changes...
A pseudo-resolution (my terminology) of `M` is a complex `C` such that `∀ i, RⁱF(C) = 0` implies `∀ i, RⁱF(M) = 0`. MacLane's Q' construction has been formalised. Now...
- [x] Construct the set-theoretic maps φ : ℒ → ℒ and θ : ℒ → ℳ and show that the first is injective and its image coincides with the...