Johan Commelin
Johan Commelin
https://leanprover-community.github.io/theories/linear_algebra.html doesn't mention semilinear maps.
https://leanprover-community.github.io/100.html and https://leanprover-community.github.io/overview.html should have toggles to show/hide items that are todo/done.
A first start provided by @Vierkantor : https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/big.20ops/near/195941698 ```` when deciding how to pretty-print an expression, Lean looks up the notations associated to the head of the expression (e.g. `finset.sum`)....
Currently perfectoid ring extends Tate ring. This is cluttering the properties in perfectoid ring. I think we should remove the extension, and prove an instance from perfectoid ring to Tate...
We should have a function that decapitalizes initial clusters of uppercase letters, as that's how the naming convention works. See also: https://github.com/leanprover-community/mathport/pull/219/files/c1690c803df3b33db0fae93d1e911245a78444fd#r1081895321
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...
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...