Pull requests: leanprover-community/mathlib4

987 Open 13,280 Closed

Author

Filter by author

Loading

author:

Filter by this user

Label

Filter by label

Loading

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

Assigned to nobody Loading

assignee:

Filter by this user

Sort

Sort by

Newest Oldest Most commented Least commented Recently updated Least recently updated Best match

Most reactions

👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(Algebra/Homology): boundaries of embeddings of complex shapes t-category-theory Category theory

#14650 opened Jul 11, 2024 by joelriou Loading…

1

feat(Algebra/Homology): support of embeddings of complex shapes t-category-theory Category theory

#14649 opened Jul 11, 2024 by joelriou Loading…

1

chore(Data.Complex): add @[simp] to Complex.conj_ofReal

#14648 opened Jul 11, 2024 by Vierkantor Loading…

5

chore: move 300 lines off Combinatorics/SimpleGraph/Connectivity RFC Request for comment t-combinatorics Combinatorics tech debt tracking cross-cutting technical debt

#14647 opened Jul 11, 2024 by grunweg Loading…

4

feat(MeasureTheory/Function): Uniform tightness of functions in Lp new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory

#14646 opened Jul 11, 2024 by igorkhavkine Loading…

13

chore: remove bit0 and bit1

#14644 opened Jul 11, 2024 by jcommelin Loading…

3

feat(RingTheory/Localization/NumDem): add lemmas new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields etc)

#14643 opened Jul 11, 2024 by Command-Master Loading…

7

chore(Mathlib/Init/ZeroOne): rename Mathlib.Init.ZeroOne to Mathlib.Algebra.ZeroOne awaiting-CI tech debt tracking cross-cutting technical debt

#14642 opened Jul 11, 2024 by Komyyy Loading…

9

feat(RingTheory/Valuation/Basic): add lemmas new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields etc)

#14641 opened Jul 11, 2024 by Command-Master Loading…

1

feat(FieldTheory/IntermediateField): add restrictUniverse new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields etc)

#14640 opened Jul 11, 2024 by Command-Master Loading…

1

feat(Algebra/Algebra/Defs): add missing coe lemmas for algebraMap new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields etc)

#14639 opened Jul 11, 2024 by Command-Master Loading…

2

feat: make nonZeroDivisors.ne_zero simp new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields etc)

#14637 opened Jul 11, 2024 by Command-Master Loading…

7

feat(to_additive): unfold lemmas generated by simp t-meta Tactics, attributes or user commands

#14628 opened Jul 10, 2024 by fpvandoorn Loading…

6

feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

#14627 opened Jul 10, 2024 by Multramate Loading…

2

chore: remove porting notes 'in std' porting-notes Mathlib3 to Mathlib4 porting notes.

#14625 opened Jul 10, 2024 by grunweg Loading…

3

feat(Combinatorics/SimpleGraph): Existence of odd component blocked-by-other-PR This PR depends on another PR to Mathlib t-combinatorics Combinatorics

#14623 opened Jul 10, 2024 by pimotte Loading…

2 tasks

2

feat(Algebra/BigOperators/Group/Finset): Lemma for product being a square t-algebra Algebra (groups, rings, fields etc)

#14622 opened Jul 10, 2024 by pimotte Loading…

1

chore: remove several stray sections

#14620 opened Jul 10, 2024 by grunweg Loading…

1

chore: Merge Trunc to Squash new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! WIP Work in progress

#14619 opened Jul 10, 2024 by Command-Master • Draft

1

feat(LightCondensed): the fully faithful embedding of sequential spaces in light condensed sets blocked-by-other-PR This PR depends on another PR to Mathlib t-category-theory Category theory t-condensed Condensed mathematics t-topology Topological spaces, uniform spaces, metric spaces, filters

#14618 opened Jul 10, 2024 by dagurtomas Loading…

1 of 6 tasks

2

chore: remove superfluous intros awaiting-author A reviewer has asked the author a question or requested changes

#14614 opened Jul 10, 2024 by mo271 Loading…

7

chore: update Mathlib dependencies 2024-07-10 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done.

#14613 opened Jul 10, 2024 by leanprover-community-mathlib4-bot Loading…

1

feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras t-algebra Algebra (groups, rings, fields etc)

#14611 opened Jul 10, 2024 by acmepjz Loading…

4

Mr more def lemma WIP Work in progress

#14610 opened Jul 10, 2024 by grunweg Loading…

17

chore(workflows): don't add or remove the 'awaiting-review' label CI Modifies the continuous integration / deployment setup tech debt tracking cross-cutting technical debt

#14609 opened Jul 10, 2024 by grunweg Loading…

8