LoreonLabsPlatform

Overview

Intelligence

Markets
Builders
Research
Ecosystems
Launchpads

Search

Lean

mathlib4

(My fork of) The math library of Lean 4

LeanEmerging

Stars

1

Forks

—

Contributors

8

Last push

23h ago

Recent commits

Latest commits.

feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas (#36308)
7d71710Snir Broshi2mo ago
feat(Data/Finset/Filter): tag `Finset.filter_congr` as `congr` (#38695)
f884e9dSnir Broshi2mo ago
chore(RingTheory): `Module.Flat` is invariant under `ULift` (#37998)
32df576Christian Merten2mo ago
chore(CategoryTheory): use notation for `TypeCat.ofHom` (#38655)
a3fde50Dagur Asgeirsson2mo ago
chore(GroupTheory/Nilpotent): move declarations into namespace (#37175)
2af034aThomas Browning

2mo ago

feat(GroupTheory/OrderOfElement): add `iff` version of `IsOfFinOrder.prod_mk` (#38717)

1c83e3fThomas Browning2mo ago

feat(ModelTheory): Prove compactness of the type space (#32546)

ff96409Anish2mo ago

refactor(Analysis/Complex/UpperHalfPlane): deprecate old GL2Pos stuff (#38700)

9bc51f5David Loeffler2mo ago

Top contributors

Builders behind this project.

Ruben-VandeVelde