mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
TODO in future PRs - add "all triangles are isosceles" in such normed spaces - totally disconnected space - give instances of this to Z_p, Q_p, etc --- [
This PR proves the order isomorphism between blocks containing a point and subgroups containing its stabilizer. --- This is a new branch to correct the bad merge of #12050 [
Prove a weak version of the Bergelson intersectivity lemma. The proof gives the strong version, but we need natural density to state it. This is a prerequisite to Tao and...
WiP: Define M-ideals and establish basic properties. --- [](https://gitpod.io/from-referrer/)
This PR proves specific properties of blocks when the action is on a finite set --- - [x] depends on: #12023 - [x] depends on: #12049 It is a repost...
This PR proves some additional pasting lemmas and adds some general API to pullbacks. This contribution was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024. --- These...
Shows that the forgetful functor `forget T : Coalgebra T ⥤ C` for a comonad `T : C ⥤ C` creates colimits and creates any limits which `T` preserves. This...
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unreachable.20code.20reached.20in.20Lean.204.2E8.2E0/near/449286780). --- [](https://gitpod.io/from-referrer/)
This PR defines the closure of a set in a matroid, and provides some API. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
