Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,116 Open 17,668 Closed
1,116 Open 17,668 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(Algebra/Homology): API for the homology of an extension of homological complexe large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#19203 opened Nov 18, 2024 by joelriou Loading…
2 tasks
1
feat(MvPolynomial): C a = 0 ↔ a = 0 t-algebra Algebra (groups, rings, fields, etc)
#19202 opened Nov 18, 2024 by YaelDillies Loading…
1
feat(MvPolynomial): more lemmas about finSuccEquiv t-algebra Algebra (groups, rings, fields, etc)
#19201 opened Nov 18, 2024 by YaelDillies Loading…
1
feat(CategoryTheory): expand the API for AB axioms large-import Automatically added label for PRs with a significant increase in transitive imports
#19200 opened Nov 18, 2024 by dagurtomas Loading…
1
feat(CategoryTheory): split up a product into a binary product t-category-theory Category theory
#19199 opened Nov 18, 2024 by dagurtomas Loading…
1
feat(Algebra/Homology): the homology of an extension of homological complexes blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-category-theory Category theory
#19198 opened Nov 18, 2024 by joelriou Loading…
1 task
2
chore: deprecate LinearOrderedCommGroupWithZero lemmas blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#19197 opened Nov 18, 2024 by YaelDillies Loading…
1 task
3
feat(CategoryTheory): weaken assumptions and dualize file Limits/Constructions/Filtered.lean t-category-theory Category theory
#19196 opened Nov 18, 2024 by dagurtomas Loading…
1
feat(CategoryTheory): add Pi.map_isIso and hasProductsOfShape_of_hasProducts + duals t-category-theory Category theory
#19195 opened Nov 18, 2024 by dagurtomas Loading…
1
chore: split Topology.UniformSpace.Basic t-topology Topological spaces, uniform spaces, metric spaces, filters
#19194 opened Nov 18, 2024 by kim-em Loading…
3
refactor: make LinearOrderedCommMonoidWithZero extend OrderBot t-algebra Algebra (groups, rings, fields, etc) t-order Order theory
#19193 opened Nov 18, 2024 by YaelDillies Loading…
1
feat(CategoryTheory): add some API for countable products and countable filtered colimits t-category-theory Category theory
#19192 opened Nov 18, 2024 by dagurtomas Loading…
1
feat: right-division as an OrderIso t-algebra Algebra (groups, rings, fields, etc) t-order Order theory
#19191 opened Nov 18, 2024 by YaelDillies Loading…
1
feat(CategoryTheory): a biproduct of epimorphisms is an epimorphism, etc t-category-theory Category theory
#19190 opened Nov 18, 2024 by dagurtomas Loading…
1
feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers t-set-theory Set theory
#19189 opened Nov 18, 2024 by YnirPaz Loading…
1
feat: add Subgroup.index_mono and Subgroup.index_strict_mono t-algebra Algebra (groups, rings, fields, etc)
#19188 opened Nov 18, 2024 by riccardobrasca Loading…
1
chore: move Fin material earlier auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
#19186 opened Nov 18, 2024 by YaelDillies Loading…
4
fix: do not count un-deprecations in Mathlib/Deprecated delegated
#19184 opened Nov 18, 2024 by adomani Loading…
7
chore(FieldTheory/PurelyInseparable): fix typo _of_isIntegral' -> _of_isSeparable' easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#19182 opened Nov 18, 2024 by acmepjz Loading…
1
chore: cleanup of many set_option deprecated.linter false
#19181 opened Nov 18, 2024 by kim-em Loading…
8
feat(GroupTheory/SpecificGroups/Cyclic): Cardinality of automorphism group t-algebra Algebra (groups, rings, fields, etc)
#19180 opened Nov 18, 2024 by tb65536 Loading…
1
feat: add Nat.digits_base_pow_mul and Nat.digits_append_zeroes_append_digits t-data Data (lists, quotients, numbers, etc)
#19179 opened Nov 18, 2024 by dwrensha Loading…
1
chore(MeasureTheory): move Measure.comap to a new file maintainer-merge t-measure-probability Measure theory / Probability theory
#19178 opened Nov 18, 2024 by urkud Loading…
3
test: the findDefEqAbuse linter large-import Automatically added label for PRs with a significant increase in transitive imports
#19177 opened Nov 18, 2024 by adomani • Draft
1
chore: adaptations for nightly-2024-11-15
#19175 opened Nov 17, 2024 by kim-em Loading…
1
ProTip! Add no:assignee to see everything that’s not assigned.