Pull Requests leanprover-community/mathlib

[Merged by Bors] - chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds ready-to-merge delegated mathport

#19212 by urkud was closed 2023-06-23 00:05

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

#19211 by github-actions[bot] was closed 2023-06-22 06:31

feat(topology/algebra/module/alternating): new file awaiting-author t-analysis t-differential-geometry modifies-synchronized-file

#19210 by urkud was closed 2023-07-02 21:34

[Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions ready-to-merge t-differential-geometry wait-requested-on

#19209 by hrmacbeth was closed 2023-06-21 10:32

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

#19208 by github-actions[bot] was closed 2023-06-21 07:24

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

#19207 by github-actions[bot] was closed 2023-06-20 07:12

feat(combinatorics/simple_graph): Triangle counting RFC awaiting-review t-combinatorics modifies-synchronized-file not-too-late

#19206 by YaelDillies was closed 2023-12-08 11:19

make it a def WIP awaiting-CI modifies-synchronized-file

#19205 by riccardobrasca was closed 2023-06-19 19:05

[Merged by Bors] - refactor(data/matrix/invertible): more results about invertible matrices ready-to-merge delegated modifies-synchronized-file wait-requested-on

#19204 by eric-wieser was closed 2023-06-21 02:06

[Merged by Bors] - feat(combinatorics/simple_graph): More clique lemmas ready-to-merge t-combinatorics modifies-synchronized-file not-too-late

#19203 by YaelDillies was closed 2023-10-22 23:25

feat(combinatorics/simple_graph): Construct a tripartite graph from its triangles awaiting-review t-combinatorics modifies-synchronized-file not-too-late

#19202 by YaelDillies was closed 2023-11-18 11:08

feat(combinatorics/simple_graph): Locally linear graphs awaiting-review t-combinatorics modifies-synchronized-file not-too-late

#19201 by YaelDillies was closed 2023-11-18 10:36

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

#19200 by github-actions[bot] was closed 2023-06-19 07:43

[Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average ready-to-merge t-measure-probability modifies-synchronized-file

#19199 by YaelDillies was closed 2023-06-21 09:24

[Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card ready-to-merge modifies-synchronized-file

#19198 by AntoineChambert-Loir was closed 2023-06-26 14:00

[Merged by Bors] - chore(data/zmod/algebra): make zmod.algebra a def ready-to-merge modifies-synchronized-file

#19197 by riccardobrasca was closed 2023-06-19 21:30

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

#19196 by github-actions[bot] was closed 2023-06-17 07:30

[Merged by Bors] - style(archive.100-theorems-list.xx_theorem_name): rename to `wiedijk_100_theorems.theorem_name` ready-to-merge delegated

#19195 by Komyyy was closed 2023-06-16 06:39

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

#19194 by github-actions[bot] was closed 2023-06-16 06:39

[Merged by Bors] - chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files ready-to-merge

#19193 by kim-em was closed 2023-06-16 05:28

[Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again ready-to-merge easy delegated

#19191 by riccardobrasca was closed 2023-06-15 11:22

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

#19190 by github-actions[bot] was closed 2023-06-15 06:09

[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec ready-to-merge delegated modifies-synchronized-file

#19188 by kim-em was closed 2023-06-15 15:03

[Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances ready-to-merge delegated mathport modifies-synchronized-file

#19187 by eric-wieser was closed 2023-06-14 15:43

[Merged by Bors] - feat(measure_theory/constructions/polish): quotient group is a Borel space ready-to-merge mathport modifies-synchronized-file

#19186 by urkud was closed 2023-06-14 17:47

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

#19185 by github-actions[bot] was closed 2023-06-14 05:58

[Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove `open_locale classical` ready-to-merge delegated

#19184 by eric-wieser was closed 2023-06-14 15:43

[Merged by Bors] - chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` ready-to-merge easy modifies-synchronized-file

#19183 by eric-wieser was closed 2023-06-14 10:32

[Merged by Bors] - refactor(data/polynomial/ring_division): remove `open_locale classical` ready-to-merge delegated modifies-synchronized-file

#19182 by eric-wieser was closed 2023-06-13 09:01

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

#19181 by github-actions[bot] was closed 2023-06-13 07:06