Pull Requests leanprover-community/mathlib3

old WIP trying to replace fractional_ideal by submodule in class_group: to be ported

#19245 by alreadydone was closed 2024-06-28 02:36

refactor: Remove the K argument from exp modifies-synchronized-file too-late

#19244 by eric-wieser was closed 2023-11-12 17:29

[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme ready-to-merge docs not-too-late

#19243 by eric-wieser was closed 2023-10-11 00:15

chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma easy awaiting-review awaiting-CI t-algebra modifies-synchronized-file

#19242 by eric-wieser was closed 2023-09-27 10:39

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19239 by github-actions[bot] was closed 2023-07-22 10:17

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization not-too-late

#19238 by github-actions[bot] was closed 2023-07-16 14:02

[Merged by Bors] - fix: handle archive and counterexamples correctly when adding port comments ready-to-merge CI not-too-late

#19237 by eric-wieser was closed 2023-07-16 12:11

[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex` ready-to-merge t-algebra modifies-synchronized-file not-too-late

#19236 by eric-wieser was closed 2023-07-28 12:00

[Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs ready-to-merge delegated t-algebra modifies-synchronized-file

#19235 by eric-wieser was closed 2023-07-13 13:57

[Merged by Bors] - chore(ring_theory/kaehler): cleanup instances ready-to-merge t-algebra modifies-synchronized-file not-too-late

#19234 by eric-wieser was closed 2023-07-24 08:56

[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith ready-to-merge t-meta not-too-late

#19233 by eric-wieser was closed 2023-07-16 12:11

[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars ready-to-merge t-meta delegated

#19232 by eric-wieser was closed 2023-07-12 18:27

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19231 by github-actions[bot] was closed 2023-07-15 14:47

[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 ready-to-merge delegated modifies-synchronized-file

#19230 by kim-em was closed 2023-07-04 08:21

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19229 by github-actions[bot] was closed 2023-07-08 13:42

[Merged by Bors] - fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument bug ready-to-merge t-meta

#19228 by Komyyy was closed 2023-07-12 21:38

[Merged by Bors] - chore(scripts): update nolints.txt

#19227 by ghost was closed 2023-07-01 05:29

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19226 by github-actions[bot] was closed 2023-07-03 07:26

refactor: change notation for interval integrals RFC awaiting-review modifies-synchronized-file too-late

#19225 by urkud was closed 2024-06-20 04:06

feat(topology/order): Add closure.mono awaiting-review modifies-synchronized-file

#19224 by mans0954 was closed 2023-06-30 17:44

[Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file ready-to-merge mathport modifies-synchronized-file

#19223 by urkud was closed 2023-06-30 15:09

[Merged by Bors] - chore(category_theory/concrete_category): reorder universes ready-to-merge modifies-synchronized-file

#19222 by kim-em was closed 2023-06-30 05:27

[Merged by Bors] - refactor: redefine `bundle.total_space` ready-to-merge mathport modifies-synchronized-file

#19221 by urkud was closed 2023-07-02 15:47

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19220 by github-actions[bot] was closed 2023-06-30 16:32

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19218 by github-actions[bot] was closed 2023-06-29 16:04

[Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic ready-to-merge

#19217 by kim-em was closed 2023-06-27 05:32

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19216 by github-actions[bot] was closed 2023-06-28 07:16

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19215 by github-actions[bot] was closed 2023-06-26 05:58

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19214 by github-actions[bot] was closed 2023-06-24 07:43

[Merged by Bors] - chore(*): add mathlib4 synchronization comments ready-to-merge easy mathlib4-synchronization

#19213 by github-actions[bot] was closed 2023-06-23 08:09