Pull Requests leanprover-community/mathlib

[Merged by Bors] - chore(field_theory/abel_ruffini): Rename variables ready-to-merge

#19180 by tb65536 was closed 2023-06-13 09:01

[Merged by Bors] - refactor(field_theory/splitting_field/is_splitting_field): use `root_set` ready-to-merge mathport modifies-synchronized-file

#19179 by eric-wieser was closed 2023-06-12 21:06

[Merged by Bors] - chore(field_theory/splitting_field): refactor `splitting_field` ready-to-merge mathport

#19178 by riccardobrasca was closed 2023-06-15 07:41

[Merged by Bors] - chore(measure_theory/function/conditional_expectation): split `measure_theory.function.conditional_expectation.basic` ready-to-merge delegated mathport

#19177 by RemyDegenne was closed 2023-06-12 10:40

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

#19176 by github-actions[bot] was closed 2023-06-12 07:43

[Merged by Bors] - feat(order/monotone): add `decidable` instances ready-to-merge easy modifies-synchronized-file

#19175 by ericrbg was closed 2023-06-22 02:23

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

#19174 by github-actions[bot] was closed 2023-06-11 08:09

chore(number_theory/wilson): reduce imports awaiting-review awaiting-CI

#19173 by kim-em was closed 2023-06-10 08:41

[Merged by Bors] - chore(number_theory/legendre_symbol/gauss_eisenstein_lemmas): move zmod.wilsons_lemma delegated

#19172 by Ruben-VandeVelde was closed 2023-06-10 21:05

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

#19171 by github-actions[bot] was closed 2023-06-10 06:47

[Merged by Bors] - refactor(representation_theory/Rep): define `ihom` concretely ready-to-merge

#19170 by 101damnations was closed 2023-06-13 02:28

[Merged by Bors] - chore(*): fix `@[to_additive, simp]` to the correct order ready-to-merge modifies-synchronized-file

#19169 by ericrbg was closed 2023-06-14 13:43

[Merged by Bors] - chore(*/centralizer): add forgotten `to_additive`s ready-to-merge modifies-synchronized-file

#19168 by ericrbg was closed 2023-06-09 17:26

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

#19167 by github-actions[bot] was closed 2023-06-09 07:26

[Merged by Bors] - chore(modular_forms/basic): fix typo in docs ready-to-merge easy docs

#19166 by ericrbg was closed 2023-06-09 08:30

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

#19165 by github-actions[bot] was closed 2023-06-08 06:02

[Merged by Bors] - refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports ready-to-merge delegated

#19164 by kim-em was closed 2023-06-07 11:35

[Merged by Bors] - chore(linear_algebra/eigenspace): split file ready-to-merge

#19163 by kim-em was closed 2023-06-07 07:54

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

#19162 by github-actions[bot] was closed 2023-06-07 06:46

[Merged by Bors] - chore(algebra/algebra/spectrum): split file delegated

#19161 by j-loreaux was closed 2023-06-06 18:21

[Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure ready-to-merge delegated t-measure-probability

#19160 by RemyDegenne was closed 2023-06-07 12:40

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

#19159 by github-actions[bot] was closed 2023-06-06 06:35

[Merged by Bors] - feat (number_theory/zeta_function): func eqn + link to Bernoulli nos delegated

#19158 by loefflerd was closed 2023-06-07 09:01

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

#19157 by github-actions[bot] was closed 2023-06-05 08:23

[Merged by Bors] - feat(linear_algebra/matrix/schur_complement): invertibility of block matrices ready-to-merge t-algebra modifies-synchronized-file wait-requested-on

#19156 by eric-wieser was closed 2023-07-02 08:07

[Merged by Bors] - chore(archive/imo): fix some naming inconsistencies and whitespace delegated

#19155 by adomani was closed 2023-06-05 03:24

[Merged by Bors] - chore(field_theory/splitting_field): split file ready-to-merge

#19154 by riccardobrasca was closed 2023-06-05 06:26

[Merged by Bors] - chore(topology/sheaves/*): universe generalizations ready-to-merge modifies-synchronized-file

#19153 by kim-em was closed 2023-06-04 17:38

[Merged by Bors] - chore(archive/imo): change namespace `imo` to `imoYYYY_qX` ready-to-merge

#19152 by adomani was closed 2023-06-04 12:08

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

#19151 by github-actions[bot] was closed 2023-06-04 06:56