leanprover-community/mathlib4 issues and pull requests

#12416 - chore: remove some cdots

Pull Request - State: open - Opened by adomani 2 months ago

#12415 - feat(Data/Matroid/Constructions): simple constructions of matroids

Pull Request - State: open - Opened by apnelson1 2 months ago

#12414 - test: lint and unlint `·`

Pull Request - State: open - Opened by adomani 2 months ago - 2 comments

#12413 - chore(Combinatorics/SimpleGraph): Generalize few lemmas in `AdjMatrix` to `NonAssocSemiring α`

Pull Request - State: open - Opened by Rida-Hamadani 2 months ago
Labels: awaiting-review, easy, t-combinatorics

#12412 - perf: speed up slow NumberTheory file

Pull Request - State: open - Opened by MichaelStollBayreuth 2 months ago - 2 comments
Labels: WIP

#12411 - feat: more linting of cdots

Pull Request - State: open - Opened by adomani 2 months ago - 2 comments

#12410 - perf: disable #align and friends to see what this gains in performance

Pull Request - State: open - Opened by MichaelStollBayreuth 2 months ago - 3 comments
Labels: WIP

#12409 - chore: update/fix two porting notes referring to an old nightly

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, porting-notes

#12408 - chore(CategoryTheory,Combinatorics,FieldTheory,Geometry): add a few more deprecation dates

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, tech debt

#12407 - chore(LinearAlgebra): format/add dates to remaining deprecations

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, tech debt

#12406 - chore(GroupTheory): reformat deprecation dates

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, easy, tech debt

#12405 - feat(Analysis/BoxIntegral): Add `UnitPartition`

Pull Request - State: open - Opened by xroblot 2 months ago
Labels: WIP, t-analysis

#12404 - feat(PseudoMetric) : TotallyBounded -> Separable

Pull Request - State: open - Opened by JADekker 2 months ago
Labels: awaiting-review, easy, t-topology

#12403 - feat: clean-up `Topology.Order.IntermediateValue`

Pull Request - State: open - Opened by fpvandoorn 2 months ago
Labels: awaiting-review

#12402 - feat(Topology/ContinuousFunction/CompactlySupported) bundle the class of compactly supported continuous functions

Pull Request - State: open - Opened by yoh-tanimoto 2 months ago
Labels: WIP, awaiting-review, RFC, t-topology, new-contributor

#12401 - chore: Move UFD instance for `Nat`

Pull Request - State: open - Opened by YaelDillies 2 months ago
Labels: awaiting-review, t-algebra

#12400 - feat: add instances for Measure.pi

Pull Request - State: open - Opened by LorenzoLuccioli 2 months ago
Labels: t-measure-probability, new-contributor

#12399 - feat: add ac_zero_iff

Pull Request - State: open - Opened by LorenzoLuccioli 2 months ago
Labels: t-measure-probability, new-contributor

#12398 - chore(Data/Set/List): nthLe -> get migration

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, easy, tech debt

#12397 - chore(Data/List/Perm): some nthLe -> get migration

Pull Request - State: open - Opened by grunweg 2 months ago
Labels: awaiting-review, tech debt

#12396 - feat : define separable measures

Pull Request - State: open - Opened by JADekker 2 months ago
Labels: WIP

#12395 - feat: add MeasurableEquiv.piOptionEquivProd

Pull Request - State: open - Opened by LorenzoLuccioli 2 months ago
Labels: t-measure-probability, new-contributor

#12394 - feat : define pre-tight and tight measures

Pull Request - State: open - Opened by JADekker 2 months ago
Labels: WIP

#12393 - chore: split CategoryTheory.MorphismProperty

Pull Request - State: open - Opened by joelriou 2 months ago - 2 comments
Labels: awaiting-review, t-category-theory

#12392 - [Merged by Bors] - feat(RingTheory/MvPolynomial): freeness of `MvPolynomial`

Pull Request - State: closed - Opened by judithludwig 2 months ago - 2 comments
Labels: ready-to-merge, t-algebra, new-contributor

#12391 - [Merged by Bors] - feat(GroupTheory): add lemmas about `Submonoid.closure` and `CoprodI`

Pull Request - State: closed - Opened by urkud 2 months ago - 4 comments
Labels: delegated, ready-to-merge, t-algebra

#12390 - [Merged by Bors] - doc(Algebra/Lie): fix typo

Pull Request - State: closed - Opened by frederic-marbach 2 months ago - 2 comments
Labels: documentation, ready-to-merge, easy

#12389 - [Merged by Bors] - chore: minor backports

Pull Request - State: closed - Opened by semorrison 2 months ago - 2 comments
Labels: ready-to-merge, easy

#12388 - feat(List/EraseIdx): new file

Pull Request - State: open - Opened by urkud 2 months ago - 1 comment
Labels: awaiting-review, t-logic

#12387 - π-base proof of concept

Pull Request - State: open - Opened by StevenClontz 2 months ago - 1 comment

#12386 - perf(NumberTheory.NumberField.Basic): make `RingOfIntegers` a Type.

Pull Request - State: open - Opened by riccardobrasca 2 months ago - 2 comments
Labels: awaiting-review, t-number-theory, t-algebra

#12385 - feat: `mapsTo`, `surjOn` and `injOn` are preserved by `Filter.map`

Pull Request - State: open - Opened by ADedecker 2 months ago - 1 comment
Labels: delegated, t-topology

#12384 - [Merged by Bors] - feat(CategoryTheory/EqToHom): generalize Functor.congr_map to Prefunctor.congr_map

Pull Request - State: closed - Opened by callesonne 2 months ago - 2 comments
Labels: ready-to-merge, t-category-theory, new-contributor

#12383 - feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure

Pull Request - State: open - Opened by callesonne 2 months ago - 1 comment
Labels: awaiting-author, t-category-theory, new-contributor

#12381 - chore: adapt to multiple goal linter 4

Pull Request - State: open - Opened by adomani 2 months ago
Labels: awaiting-review, merge-conflict

#12380 - feat: direct sum of matroids

Pull Request - State: open - Opened by madvorak 2 months ago - 3 comments
Labels: awaiting-review

#12378 - chore: move LinearMap.range into its own file

Pull Request - State: open - Opened by Ruben-VandeVelde 2 months ago - 1 comment
Labels: delegated

#12374 - feat(CategoryTheory/Sites): the category of sheaves is a localization of the category of presheaves

Pull Request - State: open - Opened by joelriou 2 months ago - 4 comments
Labels: WIP, t-category-theory

#12367 - [Merged by Bors] - chore(Data/List/Basic): remove some long-deprecated unused lemmas

Pull Request - State: closed - Opened by grunweg 2 months ago - 3 comments
Labels: ready-to-merge, easy, tech debt

#12366 - feat: add easy lemma about measure and symmetric difference

Pull Request - State: closed - Opened by EtienneC30 2 months ago - 3 comments
Labels: awaiting-review, t-measure-probability, new-contributor

#12365 - [Merged by Bors] - chore: move gcd_eq_one_of_gcd_mul_right_eq_one_* earlier

Pull Request - State: closed - Opened by Ruben-VandeVelde 2 months ago - 8 comments
Labels: delegated, ready-to-merge, maintainer-merge

#12364 - chore: move NormalizedGCDMonoid ℤ to reduce imports

Pull Request - State: open - Opened by Ruben-VandeVelde 2 months ago - 2 comments
Labels: awaiting-author

#12363 - chore(CategoryTheory/Adjunction): move `Adjunction.restrictFullyFaithful` to separate file

Pull Request - State: open - Opened by dagurtomas 2 months ago - 2 comments
Labels: awaiting-author, t-category-theory

#12361 - chore: adapt to multiple goal linter 2

Pull Request - State: open - Opened by adomani 2 months ago
Labels: awaiting-review

#12352 - draft: combining the multiple goal linter and the current modifications

Pull Request - State: open - Opened by adomani 2 months ago

#12350 - chore(Data/List): remove some long-deprecated theorems

Pull Request - State: open - Opened by grunweg 2 months ago - 1 comment
Labels: blocked-by-other-PR, awaiting-review, merge-conflict, tech debt

#12348 - [Merged by Bors] - feat: add a rfl lemma about non negative norm seen as en ENNReal

Pull Request - State: closed - Opened by EtienneC30 2 months ago - 2 comments
Labels: ready-to-merge, easy, t-analysis, new-contributor

#12340 - [Merged by Bors] - feat: add 3 lemmas linking iSup and symmDiff

Pull Request - State: closed - Opened by EtienneC30 2 months ago - 4 comments
Labels: delegated, t-order, new-contributor

#12338 - chore: adapt to multiple goal linter 1

Pull Request - State: open - Opened by adomani 2 months ago - 2 comments
Labels: awaiting-review, merge-conflict

#12337 - [Merged by Bors] - chore(Data/List): add dates to all deprecated lemmas

Pull Request - State: closed - Opened by grunweg 2 months ago - 6 comments
Labels: delegated

#12336 - [Merged by Bors] - chore(Analysis): add missing deprecation dates

Pull Request - State: closed - Opened by grunweg 2 months ago - 2 comments
Labels: ready-to-merge

#12335 - [Merged by Bors] - chore: reformat deprecation warnings on one line, if possible

Pull Request - State: closed - Opened by grunweg 2 months ago - 2 comments
Labels: ready-to-merge, tech debt

#12334 - [Merged by Bors] - chore: unify date formatting in lemma deprecations

Pull Request - State: closed - Opened by grunweg 2 months ago - 3 comments
Labels: ready-to-merge, tech debt

#12331 - chore: replace `refine ?_` and `refine' _` by `apply`

Pull Request - State: open - Opened by mo271 2 months ago - 1 comment
Labels: merge-conflict

#12330 - chore: remove redundant LinearEquiv.map_neg/sub

Pull Request - State: open - Opened by Ruben-VandeVelde 2 months ago
Labels: awaiting-author

#12327 - [Merged by Bors] - feat(Inseparable): `Prod.map mk mk` is a quotient map

Pull Request - State: closed - Opened by urkud 2 months ago - 2 comments
Labels: ready-to-merge, easy, t-topology

#12326 - [Merged by Bors] - feat(List): add lemmas about `Sublist`

Pull Request - State: closed - Opened by urkud 2 months ago - 2 comments
Labels: ready-to-merge, t-logic

#12319 - [Merged by Bors] - refactor(QuadraticForm/Real): migrate to `SignType`

Pull Request - State: closed - Opened by urkud 3 months ago - 2 comments
Labels: ready-to-merge, t-algebra

#12316 - [Merged by Bors] - chore: tidy various files

Pull Request - State: closed - Opened by Ruben-VandeVelde 3 months ago - 3 comments
Labels: delegated

#12304 - [Merged by Bors] - feat(List/Basic): add `get_eq_get?`

Pull Request - State: closed - Opened by urkud 3 months ago - 4 comments
Labels: ready-to-merge, auto-merge-after-CI, t-logic

#12302 - [Merged by Bors] - chore(Perm/List): golf, review API

Pull Request - State: closed - Opened by urkud 3 months ago - 2 comments
Labels: ready-to-merge, t-logic

#12297 - feat(Algebra/Lie): existence of Cartan subalgebras

Pull Request - State: open - Opened by jcommelin 3 months ago
Labels: WIP

#12290 - feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

Pull Request - State: open - Opened by yoh-tanimoto 3 months ago - 10 comments
Labels: WIP, RFC, t-measure-probability, new-contributor

#12285 - [Merged by Bors] - Bugfix Polyrith.lean

Pull Request - State: closed - Opened by todbeibrot 3 months ago - 3 comments
Labels: ready-to-merge, easy, t-meta, new-contributor

#12247 - feat (RingTheory/Valuation/Integers) : add lemma one_of_isUnit'

Pull Request - State: open - Opened by faenuccio 3 months ago - 3 comments
Labels: awaiting-review, t-algebra, maintainer-merge

#12246 - [Merged by Bors] - feat(Nat/GCD): Add dvd_gcd_mul_gcd_of_dvd_mul

Pull Request - State: closed - Opened by Jun2M 3 months ago - 2 comments
Labels: ready-to-merge, new-contributor

#12244 - feat: make `rank_mul_eq_left_of_isUnit_det` into an effective `simp` lemma

Pull Request - State: open - Opened by JonBannon 3 months ago - 4 comments
Labels: awaiting-review, new-contributor

#12237 - [Merged by Bors] - feat: `∃! x ∈ s, p x` syntax

Pull Request - State: closed - Opened by kmill 3 months ago - 2 comments
Labels: ready-to-merge

#12171 - [Merged by Bors] - feat(List/rotate): migrate to `get`, new lemmas, golf

Pull Request - State: closed - Opened by urkud 3 months ago - 5 comments
Labels: delegated, tech debt

#12144 - feat: Fourier transform as a continuous linear equiv on Schwartz space

Pull Request - State: open - Opened by sgouezel 3 months ago - 1 comment
Labels: blocked-by-other-PR, t-analysis

#12143 - feat: a `cdot` linter

Pull Request - State: open - Opened by adomani 3 months ago - 2 comments
Labels: awaiting-review, merge-conflict, t-linter

#12086 - feat(List/Basic): Add lemmas relating head(!?) with getLast(!?) through reverse

Pull Request - State: closed - Opened by Jun2M 3 months ago
Labels: awaiting-author, merge-conflict, new-contributor

#11986 - chore: Move sign of power lemmas

Pull Request - State: open - Opened by YaelDillies 3 months ago - 2 comments
Labels: awaiting-review, t-algebra, t-order

#11969 - feat(List/Enum): add lemmas

Pull Request - State: open - Opened by urkud 3 months ago - 3 comments
Labels: delegated, merge-conflict, t-logic

#11960 - feat: port `cc` tactic (2/3)

Pull Request - State: open - Opened by Komyyy 3 months ago - 1 comment
Labels: awaiting-review, mathlib-port, t-meta

#11956 - [Merged by Bors] - feat: port `cc` tactic (1/3)

Pull Request - State: closed - Opened by Komyyy 3 months ago - 5 comments
Labels: delegated, mathlib-port, t-meta

#11888 - feat(Algebra/BigOperators/Associated): add lemma Associated_closure_of_mul_mem_closure

Pull Request - State: open - Opened by EmilieUthaiwat 3 months ago
Labels: WIP, awaiting-author, t-algebra

#11774 - Feat: Define cocardinal and cocountable filters

Pull Request - State: open - Opened by JADekker 3 months ago - 1 comment
Labels: delegated, t-topology

#11765 - [Merged by Bors] - chore: Move intervals

Pull Request - State: closed - Opened by YaelDillies 3 months ago - 2 comments
Labels: awaiting-review, ready-to-merge, t-algebra, t-order

#11746 - feat: proper group actions

Pull Request - State: open - Opened by vin-gui 3 months ago - 2 comments
Labels: WIP, awaiting-author, awaiting-CI, t-topology, new-contributor, lftcm2024

#11633 - refactor: Lighten finiteness dependencies

Pull Request - State: open - Opened by YaelDillies 3 months ago - 1 comment
Labels: WIP, blocked-by-other-PR

#11582 - Feat: Finset builder notation

Pull Request - State: open - Opened by YaelDillies 4 months ago
Labels: awaiting-review, t-meta

#11526 - feat: add the standard geometric representation of a Coxeter group

Pull Request - State: open - Opened by trivial1711 4 months ago - 2 comments
Labels: blocked-by-other-PR, awaiting-review, new-contributor

#11406 - feat: simple reflections, words, lifting in Coxeter groups

Pull Request - State: open - Opened by trivial1711 4 months ago - 7 comments
Labels: awaiting-author, t-combinatorics, t-algebra, new-contributor

#11363 - New definition of eigenvectorUnitary

Pull Request - State: open - Opened by JonBannon 4 months ago - 1 comment
Labels: WIP, new-contributor

#11241 - feat(CategoryTheory/Category/RelCat): Show basic facts and self-duality of category of relations.

Pull Request - State: open - Opened by uniwuni 4 months ago - 3 comments
Labels: awaiting-author, t-category-theory

#11185 - feat: continuity of primitives for parametric integrals

Pull Request - State: open - Opened by grunweg 4 months ago - 8 comments
Labels: awaiting-author, merge-conflict, t-analysis, t-measure-probability

#11104 - move: Rearrange basic algebraic subobject

Pull Request - State: open - Opened by YaelDillies 4 months ago - 12 comments
Labels: awaiting-review, t-topology, t-algebra

#10834 - feat : FactorisationProperties (new file)

Pull Request - State: open - Opened by Colin166 4 months ago - 14 comments
Labels: WIP, awaiting-author, new-contributor

#10377 - Eisenstein series uniform convergence

Pull Request - State: open - Opened by CBirkbeck 5 months ago - 1 comment
Labels: awaiting-author, merge-conflict

#10350 - Feat(Data/Setoid): Add the operations of taking the equivalence class of an element and of saturating a set wrt an equivalence relation.

Pull Request - State: open - Opened by Shamrock-Frost 5 months ago - 1 comment
Labels: awaiting-review, merge-conflict

GitHub / leanprover-community/mathlib4 issues and pull requests