Back to search
Top Contributors
1.8k
commits
1.8k
commits
1.7k
commits
1.1k
commits
1.0k
commits
998
commits
987
commits
676
commits
663
commits
593
commits
The math library of Lean 4
Stars
3.1k
Forks
1.2k
Watchers
3.1k
Open Issues
2.6k
Overall repository health assessment
No package.json found
This might not be a Node.js project
1.8k
commits
1.8k
commits
1.7k
commits
1.1k
commits
1.0k
commits
998
commits
987
commits
676
commits
663
commits
593
commits
feat(Analysis/InnerProductSpace/Reproducing): lemmata for reproducing kernels (#37533)
de14307View on GitHubfeat(Data/Finsupp): add computational lemmas for cons and single (#35329)
35186beView on GitHubchore(Archive/Wiedijk100Theorems/BirthdayProblem): cleanup (#37679)
5948832View on GitHubchore(RepresentationTheory/Intertwining): slightly generalise two lemmas (#37694)
39328e9View on GitHubfeat: weaken assumptions on lemmas about `FloorRing` (#37582)
03cf4f1View on GitHubfeat(NumberTheory/Modular): strengthen 2nd Fundamental-Domain Lemma (#36736)
29f21b6View on GitHubfix(GroupTheory): avoid unintentional list item continuation lines (#37615)
05c4d64View on GitHubdoc(NumberTheory): avoid lazy continuation lines (#37571)
8eda17dView on GitHubchore(MeasureTheory/Measure/MeasureSpace): reduce `privateInPublic` (#37657)
ae0c614View on GitHubchore(SetTheory/Ordinal/Topology): deprecate theorems about `Ordinal.bsup` (#37667)
7bc2841View on GitHubchore: remove unnecessary set_option lines (#37687)
be4dc1aView on GitHubrefactor(Tactic): change `ring` to allow for coefficients in a variable type (#34734)
053a003View on GitHubdoc(Data/Setoid/Partition): fix typo in module docstring (#37672)
08becbaView on GitHubrefactor: deprecate `Ordinal.lsub` (#37262)
49358d7View on GitHubfeat: pushing `Lattice` and predecessors through `Equiv` (#37605)
188fc54View on GitHub