mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
This PR contains a linter for flagging doc-string-less `theorem`s, as well as a bash script that, once the linter ran on Mathlib, automatically replaces every linter-offending `theorem` by `lemma`. ---...
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the...
Variant of `prod_Ioc_succ_top` and `prod_Ico_succ_top`. --- [](https://gitpod.io/from-referrer/)
--- - [ ] depends on: #13004 - [ ] depends on: #13011 - [ ] depends on: #13012 [](https://gitpod.io/from-referrer/)
Given a functor `F : C ⥤ D` between categories equipped with Grothendieck topologies, the condition that `F` preserves covers (developed in the file `CategoryTheory.Sites.CoverPreserving`) does not obviously imply that...
In this PR, we show that a Grothendieck topology on a category `C` (with `C : Type u` and `[Category.{v} C]`) is (obviously) generated by 1-hypercovers of size `max u...
`Algebra/Module/FinitePresentation.lean` is now fully universe polymorphic. This had the side effect of somehow breaking `RingTheory/Flat/EquationalCriterion.lean`, even though I didn't even touch that file. Should I even be trying to do...
Add the theorem `pathGraph_G_Hom_coloring` saying that if a graph has a homorphism from a pathGraph then the colors alternate in the path. Specifically, the theorem ask for the first element...
--- - [ ] depends on: #12597 [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)