From 7d526cd198e1f9a74800ad65c7531f825ec70672 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 3 Aug 2022 01:01:07 +0200
Subject: [PATCH 1/5] add data and script

---
 get_month.py                       |  72 +++++
 posts/month-in-mathlib-jul-2022.md | 417 +++++++++++++++++++++++++++++
 2 files changed, 489 insertions(+)
 create mode 100644 get_month.py
 create mode 100644 posts/month-in-mathlib-jul-2022.md

diff --git a/get_month.py b/get_month.py
new file mode 100644
index 00000000..42f8bf07
--- /dev/null
+++ b/get_month.py
@@ -0,0 +1,72 @@
+from github import Github
+from datetime import datetime, date, time
+from dateutil.relativedelta import *
+import argparse
+
+parser = argparse.ArgumentParser()
+parser.add_argument("month", help="Month",
+                    type=int)
+parser.add_argument("year", help="Year",
+                    type=int)
+args = parser.parse_args()
+
+def extract_folder(title):
+    start = title.index('(')
+    end = title.index(')', start+1)
+    return title[start+1:end]
+
+def extract_pr_number(title):
+    words = title.split()
+    return words[-1][2:-1]
+
+def extract_msg_title(title):
+    start = title.index(')') # this is totally stupid, but some people forget the colon
+    words = title.split()
+    end = len(words[-1])
+    return title[start+2:-end].lstrip()
+
+class mathlib_commit():
+    def __init__(self, commit):
+        self.author = commit.commit.author.name
+        title = commit.commit.message.splitlines()[0]
+        self.pr = extract_pr_number(title)
+        self.folder = extract_folder(title)
+        self.msg_title = extract_msg_title(title)
+        self.feature = title.startswith("feat")
+
+g = Github()
+repo = g.get_repo("leanprover-community/mathlib")
+
+date1 = date(args.year, args.month, 1)
+date2 = date1 + relativedelta(months=+1)
+time = time(0, 0)
+
+now = datetime.now()
+
+monthnames_uc = ["NaM", "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
+monthnames_lc = ["NaM", "jan", "feb", "mar", "apr", "may", "jun", "jul", "aug", "sep", "oct", "nov", "dec"]
+
+# Get all commits in the timeframe
+commit_list = repo.get_commits(since=datetime.combine(date1,time), until=datetime.combine(date2,time))
+
+mathlib_commits = list(map(lambda commit: mathlib_commit(commit), commit_list))
+
+number_of_commits = len(mathlib_commits)
+
+sorted_commits = sorted(mathlib_commits, key=lambda commit: commit.folder)
+
+this_month_file = open("this_month_" + str(args.year) + "_" + monthnames_lc[args.month], "a")
+
+print("Number of commits: " + str(number_of_commits))
+
+print("---\nauthor: 'Mathlib community'\ncategory: 'month-in-mathlib'\ndate: " +
+        str(now) + "\ndescription: ''\nhas_math: true\nlink: ''\nslug: month-in-mathlib-" +
+        monthnames_lc[args.month] + "-" + str(args.year) +
+        "\ntags: ''\ntitle: This month in mathlib (" + monthnames_uc[args.month]
+        + " " + str(args.year) + ")\ntype: text\n---\n", file=this_month_file)
+
+for commit in sorted_commits:
+    if commit.feature:
+        print("[PR #" + commit.pr +
+                "](https://github.com/leanprover-community/mathlib/pull/" +
+                commit.pr + ")" + " " + commit.folder + ": " + commit.msg_title, file=this_month_file)
diff --git a/posts/month-in-mathlib-jul-2022.md b/posts/month-in-mathlib-jul-2022.md
new file mode 100644
index 00000000..ee832cac
--- /dev/null
+++ b/posts/month-in-mathlib-jul-2022.md
@@ -0,0 +1,417 @@
+---
+author: 'Mathlib community'
+category: 'month-in-mathlib'
+date: 2022-08-03 00:49:41.091267
+description: ''
+has_math: true
+link: ''
+slug: month-in-mathlib-jul-2022
+tags: ''
+title: This month in mathlib (Jul 2022)
+type: text
+---
+
+[PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) *: add lemmas about sigma types 
+[PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) */partition_of_unity: more lemmas based on the partition of unity 
+[PR #15744](https://github.com/leanprover-community/mathlib/pull/15744) algebra/algebra/subalgebra/basic: Swap arguments of `map` and `comap` 
+[PR #15556](https://github.com/leanprover-community/mathlib/pull/15556) algebra/big_operators: add lemmas about sum of disjoint multiset 
+[PR #15095](https://github.com/leanprover-community/mathlib/pull/15095) algebra/category: forgetful functors from modules reflect limits 
+[PR #15019](https://github.com/leanprover-community/mathlib/pull/15019) algebra/category/BoolRing: The equivalence between Boolean rings and Boolean algebras 
+[PR #15330](https://github.com/leanprover-community/mathlib/pull/15330) algebra/category/Group: The forgetful-units adjunction between `Group` and `Mon`. 
+[PR #14328](https://github.com/leanprover-community/mathlib/pull/14328) algebra/category/Module: upgrade `free : Type ⥤ Module R` to a monoidal functor 
+[PR #14720](https://github.com/leanprover-community/mathlib/pull/14720) algebra/category_theory/Group/epi_mono: about monomorphism and epimorphism in category of group 
+[PR #15654](https://github.com/leanprover-community/mathlib/pull/15654) algebra/direct_sum/decomposition: add an induction principle for `direct_sum.decomposition` class 
+[PR #15109](https://github.com/leanprover-community/mathlib/pull/15109) algebra/gcd_monoid: GCD domains are integrally closed. 
+[PR #15403](https://github.com/leanprover-community/mathlib/pull/15403) algebra/group/with_one: units of a group with zero is isomorphic to the group 
+[PR #14945](https://github.com/leanprover-community/mathlib/pull/14945) algebra/homology: homotopy equivalences are quasi-isomorphisms 
+[PR #11073](https://github.com/leanprover-community/mathlib/pull/11073) algebra/jordan: Introduce Jordan rings 
+[PR #14179](https://github.com/leanprover-community/mathlib/pull/14179) algebra/lie/cartan_subalgebra: characterise Cartan subalgebras as limiting values of upper central series 
+[PR #15675](https://github.com/leanprover-community/mathlib/pull/15675) algebra/lie/of_associative: add `commute.lie_eq` 
+[PR #15733](https://github.com/leanprover-community/mathlib/pull/15733) algebra/module: sub_mem_sup for modules over rings 
+[PR #12895](https://github.com/leanprover-community/mathlib/pull/12895) algebra/module: add injective module and Baer's criterion 
+[PR #15103](https://github.com/leanprover-community/mathlib/pull/15103) algebra/module/linear_map: use morphisms class for lemmas about linear [pre]images of `c • S` 
+[PR #14470](https://github.com/leanprover-community/mathlib/pull/14470) algebra/module/localized_module: construction of module localisation 
+[PR #15092](https://github.com/leanprover-community/mathlib/pull/15092) algebra/module/torsion: `R/I`-module structure on `M/IM`. 
+[PR #3292](https://github.com/leanprover-community/mathlib/pull/3292) algebra/order/complete_field: `conditionally_complete_linear_ordered_field`, aka the reals 
+[PR #15300](https://github.com/leanprover-community/mathlib/pull/15300) algebra/order/monoid: add lemmas `map_add` for `with_bot/top` 
+[PR #15458](https://github.com/leanprover-community/mathlib/pull/15458) algebra/order/monoid: add `one_lt_mul_iff`/`add_pos_iff` 
+[PR #15219](https://github.com/leanprover-community/mathlib/pull/15219) algebra/order/monoid: Add zero_le_three and zero_le_four 
+[PR #15267](https://github.com/leanprover-community/mathlib/pull/15267) algebra/order/monoid_lemmas: add `antitone`, `monotone_on`, and `antitone_on` lemmas 
+[PR #14761](https://github.com/leanprover-community/mathlib/pull/14761) algebra/order/monoid_lemmas_zero_lt: add some lemmas about typeclasses 
+[PR #14770](https://github.com/leanprover-community/mathlib/pull/14770) algebra/order/monoid_lemmas_zero_lt: add missing lemmas 
+[PR #15186](https://github.com/leanprover-community/mathlib/pull/15186) algebra/parity: more general odd.pos 
+[PR #15660](https://github.com/leanprover-community/mathlib/pull/15660) algebra/periodic: `fract_periodic` 
+[PR #13958](https://github.com/leanprover-community/mathlib/pull/13958) algebra/ring/{pi, prod, opposite}: add basic defs for non_unital_ring_hom 
+[PR #15291](https://github.com/leanprover-community/mathlib/pull/15291) algebraic_geometry: comap of surjective homomorphism is closed embedding 
+[PR #11649](https://github.com/leanprover-community/mathlib/pull/11649) algebraic_geometry: Intersection of affine open can be covered by common basic opens 
+[PR #14972](https://github.com/leanprover-community/mathlib/pull/14972) algebraic_geometry: Restriction of morphisms onto open sets of the target 
+[PR #15487](https://github.com/leanprover-community/mathlib/pull/15487) algebraic_geometry/AffineScheme: Affine communication lemma 
+[PR #15365](https://github.com/leanprover-community/mathlib/pull/15365) algebraic_geometry/EllipticCurve: simplify definition of discriminant 
+[PR #15436](https://github.com/leanprover-community/mathlib/pull/15436) algebraic_geometry/morphisms: Quasi-compact morphisms of schemes 
+[PR #14944](https://github.com/leanprover-community/mathlib/pull/14944) algebraic_geometry/morphisms: Basic framework for classes of morphisms between schemes 
+[PR #13397](https://github.com/leanprover-community/mathlib/pull/13397) algebraic_geometry/projective_spectrum: forward direction of homeomorphism between top_space of Proj and top_space of Spec 
+[PR #14588](https://github.com/leanprover-community/mathlib/pull/14588) algebraic_topology: alternating_coface_map_complex 
+[PR #15616](https://github.com/leanprover-community/mathlib/pull/15616) algebraic_topology/dold_kan: construction of idempotent endomorphisms 
+[PR #14044](https://github.com/leanprover-community/mathlib/pull/14044) algebraic_topology/dold_kan: technical lemmas about face maps 
+[PR #12788](https://github.com/leanprover-community/mathlib/pull/12788) algebraic_topology/fundamental_groupoid: Define simply connected spaces 
+[PR #15568](https://github.com/leanprover-community/mathlib/pull/15568) analysis/asymptotics: add `is_o*.of_pow` 
+[PR #15010](https://github.com/leanprover-community/mathlib/pull/15010) analysis/asymptotics/asymptotics: generalize, golf 
+[PR #15416](https://github.com/leanprover-community/mathlib/pull/15416) analysis/calculus: generalize `differentiable*.pow`, add `differentiable*.zpow` 
+[PR #15595](https://github.com/leanprover-community/mathlib/pull/15595) analysis/calculus/cont_diff: generalize `mul` lemmas to a normed algebra 
+[PR #15309](https://github.com/leanprover-community/mathlib/pull/15309) analysis/calculus/cont_diff: extra lemmas about cont_diff_within_at 
+[PR #15133](https://github.com/leanprover-community/mathlib/pull/15133) analysis/calculus/mean_value: remove assumption in strict_mono_on.strict_convex_on_of_deriv 
+[PR #15122](https://github.com/leanprover-community/mathlib/pull/15122) analysis/complex: equiv_real_prod_symm_apply 
+[PR #15364](https://github.com/leanprover-community/mathlib/pull/15364) analysis/complex/abs_max: add a version of the maximum modulus principle 
+[PR #15639](https://github.com/leanprover-community/mathlib/pull/15639) analysis/convex/cone: add inner_dual_cone_eq_Inter_inner_dual_cone_singleton 
+[PR #14821](https://github.com/leanprover-community/mathlib/pull/14821) analysis/convex/function: Variants of `convex_on.le_right_of_left_le` 
+[PR #15363](https://github.com/leanprover-community/mathlib/pull/15363) analysis/inner_product/calculus: [higher] differentiability to/from `euclidean_space` 
+[PR #15481](https://github.com/leanprover-community/mathlib/pull/15481) analysis/inner_product/pi_L2: a finite orthonormal family is a basis of its span 
+[PR #15540](https://github.com/leanprover-community/mathlib/pull/15540) analysis/inner_product_space: in finite dimension, hilbert basis = orthonormal basis 
+[PR #15055](https://github.com/leanprover-community/mathlib/pull/15055) analysis/inner_product_space: the Hellinger-Toeplitz theorem 
+[PR #15020](https://github.com/leanprover-community/mathlib/pull/15020) analysis/inner_product_space: add simple lemmas for the orthogonal complement 
+[PR #15514](https://github.com/leanprover-community/mathlib/pull/15514) analysis/inner_product_space/[pi_L2, l2_space]: compute inner product in a given [orthonormal, hilbert] basis 
+[PR #15577](https://github.com/leanprover-community/mathlib/pull/15577) analysis/inner_product_space/basic: `orthonormal` version of `linear_independent.coe_range` 
+[PR #15470](https://github.com/leanprover-community/mathlib/pull/15470) analysis/inner_product_space/positive: definition and basic facts about positive operators 
+[PR #14876](https://github.com/leanprover-community/mathlib/pull/14876) analysis/locally_convex/basic: a few lemmas about balanced sets 
+[PR #15124](https://github.com/leanprover-community/mathlib/pull/15124) analysis/locally_convex/with_seminorms: in a normed space, von Neumann bounded = metric bounded 
+[PR #15515](https://github.com/leanprover-community/mathlib/pull/15515) analysis/normed*: add instances and lemmas 
+[PR #15467](https://github.com/leanprover-community/mathlib/pull/15467) analysis/normed_space/compact_operator: definition and basic facts about compact operators 
+[PR #15650](https://github.com/leanprover-community/mathlib/pull/15650) analysis/normed_space/linear_isometry: add defs and lemmas 
+[PR #15471](https://github.com/leanprover-community/mathlib/pull/15471) analysis/normed_space/linear_isometry: `linear_equiv.of_eq` as a `linear_isometry_equiv` 
+[PR #15317](https://github.com/leanprover-community/mathlib/pull/15317) analysis/normed_space/lp_space: construct star structures on lp spaces 
+[PR #15086](https://github.com/leanprover-community/mathlib/pull/15086) analysis/normed_space/lp_space: normed_algebra structure 
+[PR #14104](https://github.com/leanprover-community/mathlib/pull/14104) analysis/normed_space/lp_space: add l_infinity ring instances 
+[PR #15578](https://github.com/leanprover-community/mathlib/pull/15578) analysis/normed_space/operator_norm: variant of `continuous_linear_equiv.has_sum` 
+[PR #15417](https://github.com/leanprover-community/mathlib/pull/15417) analysis/normed_space/operator_norm: add 2 new versions of `op_norm_le_*` 
+[PR #15173](https://github.com/leanprover-community/mathlib/pull/15173) analysis/normed_space/star/basic: make starₗᵢ apply to normed star groups 
+[PR #15125](https://github.com/leanprover-community/mathlib/pull/15125) analysis/special_functions/complex/arg: add complex.abs_eq_one_iff 
+[PR #14980](https://github.com/leanprover-community/mathlib/pull/14980) analysis/special_functions/complex/arg: `continuous_at_arg_coe_angle` 
+[PR #15506](https://github.com/leanprover-community/mathlib/pull/15506) analysis/special_functions/exp: add lemmas about `is_o`/`is_O`/`is_Theta` 
+[PR #15106](https://github.com/leanprover-community/mathlib/pull/15106) analysis/special_functions/gaussian: formula for gaussian integrals 
+[PR #15258](https://github.com/leanprover-community/mathlib/pull/15258) analysis/special_functions/polar_coord: define polar coordinates, polar change of variable formula in integrals 
+[PR #15164](https://github.com/leanprover-community/mathlib/pull/15164) analysis/special_functions/pow: drop an assumption in `is_o_log_rpow_rpow_at_top` 
+[PR #15002](https://github.com/leanprover-community/mathlib/pull/15002) analysis/special_functions/pow: Rational powers are dense 
+[PR #15651](https://github.com/leanprover-community/mathlib/pull/15651) analysis/special_functions/trigonometric/angle: equality of `cos` or `sin` 
+[PR #14988](https://github.com/leanprover-community/mathlib/pull/14988) analysis/special_functions/trigonometric/angle: equality of twice angles 
+[PR #15360](https://github.com/leanprover-community/mathlib/pull/15360) big_operators/fin: sum over elements of vector equal to `a` equals count `a` 
+[PR #14422](https://github.com/leanprover-community/mathlib/pull/14422) category_theory: construction of the localized category 
+[PR #14838](https://github.com/leanprover-community/mathlib/pull/14838) category_theory: a characterization of separating objects 
+[PR #14974](https://github.com/leanprover-community/mathlib/pull/14974) category_theory: full_of_surjective 
+[PR #15238](https://github.com/leanprover-community/mathlib/pull/15238) category_theory: a category with a small detecting set is well-powered 
+[PR #15377](https://github.com/leanprover-community/mathlib/pull/15377) category_theory: limits of essentially small indexing categories 
+[PR #14880](https://github.com/leanprover-community/mathlib/pull/14880) category_theory: (co)products and (co)separators 
+[PR #14026](https://github.com/leanprover-community/mathlib/pull/14026) category_theory: left-exact functors preserve finite limits 
+[PR #15121](https://github.com/leanprover-community/mathlib/pull/15121) category_theory/*/algebra: epi_of_epi and mono_of_mono 
+[PR #14581](https://github.com/leanprover-community/mathlib/pull/14581) category_theory/abelian/*: functors that preserve finite limits and colimits preserve exactness 
+[PR #14834](https://github.com/leanprover-community/mathlib/pull/14834) category_theory/endofunctor/algebra: Define coalgebras over an endofunctor and prove an equivalence 
+[PR #14829](https://github.com/leanprover-community/mathlib/pull/14829) category_theory/functor: preserving/reflecting monos/epis 
+[PR #14419](https://github.com/leanprover-community/mathlib/pull/14419) category_theory/limits: preserves biproducts if comparison is iso 
+[PR #14526](https://github.com/leanprover-community/mathlib/pull/14526) category_theory/limits: opposites of limit pullback cones 
+[PR #14452](https://github.com/leanprover-community/mathlib/pull/14452) category_theory/limits: bilimit from kernel 
+[PR #14948](https://github.com/leanprover-community/mathlib/pull/14948) category_theory/limits/construction: Construct finite limits from terminal objects and pullbacks 
+[PR #15269](https://github.com/leanprover-community/mathlib/pull/15269) category_theory/limits/shapes/comm_sq: opposites of is_pullback and is_pushout 
+[PR #14445](https://github.com/leanprover-community/mathlib/pull/14445) category_theory/preadditive: constructing a semiadditive structure from binary biproducts 
+[PR #15096](https://github.com/leanprover-community/mathlib/pull/15096) category_theory/preadditive: left exactness of certain hom functors 
+[PR #14832](https://github.com/leanprover-community/mathlib/pull/14832) category_theory/preadditive: projective iff coyoneda.obj preserves epimorphisms 
+[PR #15100](https://github.com/leanprover-community/mathlib/pull/15100) category_theory/preadditive/*: algebra over endofunctor preadditive and forget additive functor 
+[PR #15455](https://github.com/leanprover-community/mathlib/pull/15455) category_theory/shapes/pullbacks: Pullbacks isomorphic to the opposite of pushouts 
+[PR #14831](https://github.com/leanprover-community/mathlib/pull/14831) category_theory/yoneda: coyoneda.obj_op_op 
+[PR #15327](https://github.com/leanprover-community/mathlib/pull/15327) combinatorics/additive/behrend: Behrend's lower bound on Roth numbers 
+[PR #14070](https://github.com/leanprover-community/mathlib/pull/14070) combinatorics/additive/behrend: Behrend's construction 
+[PR #14697](https://github.com/leanprover-community/mathlib/pull/14697) combinatorics/additive/ruzsa_covering: The Ruzsa covering lemma 
+[PR #14497](https://github.com/leanprover-community/mathlib/pull/14497) combinatorics/set_family/harris_kleitman: The Harris-Kleitman inequality 
+[PR #14475](https://github.com/leanprover-community/mathlib/pull/14475) combinatorics/set_family/intersecting: Intersecting families 
+[PR #14543](https://github.com/leanprover-community/mathlib/pull/14543) combinatorics/set_family/kleitman: Kleitman's bound 
+[PR #15150](https://github.com/leanprover-community/mathlib/pull/15150) combinatorics/simple_graph/basic: `dart.to_prod` is injective 
+[PR #15156](https://github.com/leanprover-community/mathlib/pull/15156) combinatorics/simple_graph/connectivity: operations and lemmas about path type 
+[PR #15153](https://github.com/leanprover-community/mathlib/pull/15153) combinatorics/simple_graph/connectivity: simp confluence 
+[PR #15353](https://github.com/leanprover-community/mathlib/pull/15353) combinatorics/simple_graph/density: Bound on the difference between edge densities 
+[PR #14978](https://github.com/leanprover-community/mathlib/pull/14978) combinatorics/simple_graph/hasse: The Hasse diagram of `α × β` 
+[PR #14867](https://github.com/leanprover-community/mathlib/pull/14867) combinatorics/simple_graph/prod: Box product 
+[PR #13222](https://github.com/leanprover-community/mathlib/pull/13222) combinatorics/simple_graph/regularity/equitabilise: Equitabilising a partition 
+[PR #14403](https://github.com/leanprover-community/mathlib/pull/14403) combinatorics/simple_graph/subgraph: delete vertices in a subgraph 
+[PR #14877](https://github.com/leanprover-community/mathlib/pull/14877) combinatorics/simple_graph/subgraph: add `subgraph.comap` and subgraph of subgraph coercion 
+[PR #15158](https://github.com/leanprover-community/mathlib/pull/15158) combinatorics/simple_graph/trails: Euler's condition for trails  
+[PR #14034](https://github.com/leanprover-community/mathlib/pull/14034) combinatorics/simple_graph/{basic,subgraph,clique,coloring}: add induced graphs, characterization of cliques, and bounds for colorings 
+[PR #15505](https://github.com/leanprover-community/mathlib/pull/15505) computability/ackermann: the Ackermann function isn't primitive recursive 
+[PR #15280](https://github.com/leanprover-community/mathlib/pull/15280) data/countable: add `countable` typeclass 
+[PR #15337](https://github.com/leanprover-community/mathlib/pull/15337) data/fin/basic: add a reflected instance 
+[PR #15048](https://github.com/leanprover-community/mathlib/pull/15048) data/fin/tuple/basic: add lemmas for rewriting exists and forall over `n+1`-tuples 
+[PR #15607](https://github.com/leanprover-community/mathlib/pull/15607) data/finset/basic: There is exactly one set in empty types 
+[PR #15385](https://github.com/leanprover-community/mathlib/pull/15385) data/finset/basic: lemmas about `filter`, `cons`, and `disj_union` 
+[PR #15170](https://github.com/leanprover-community/mathlib/pull/15170) data/finset/basic: Add `decidable_nonempty` for finsets. 
+[PR #15011](https://github.com/leanprover-community/mathlib/pull/15011) data/finset/basic: Coercion of a product of finsets 
+[PR #15257](https://github.com/leanprover-community/mathlib/pull/15257) data/finset/fold: add lemma `fold_max_add` 
+[PR #15212](https://github.com/leanprover-community/mathlib/pull/15212) data/finset/lattice: add three*2 lemmas about `finset.max/min` 
+[PR #15435](https://github.com/leanprover-community/mathlib/pull/15435) data/finset/pointwise: Singleton arithmetic 
+[PR #15387](https://github.com/leanprover-community/mathlib/pull/15387) data/finset/powerset: More `powerset` lemmas 
+[PR #15197](https://github.com/leanprover-community/mathlib/pull/15197) data/finsupp/basic: graph of a finitely supported function 
+[PR #15155](https://github.com/leanprover-community/mathlib/pull/15155) data/finsupp/big_operators: sum of finsupp and their support 
+[PR #15080](https://github.com/leanprover-community/mathlib/pull/15080) data/fintype/basic: add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. 
+[PR #15207](https://github.com/leanprover-community/mathlib/pull/15207) data/json: helper functions for json serialization 
+[PR #15138](https://github.com/leanprover-community/mathlib/pull/15138) data/list: accessing list with fallback 
+[PR #15472](https://github.com/leanprover-community/mathlib/pull/15472) data/list/basic: when drop_while and take_while hold 
+[PR #15482](https://github.com/leanprover-community/mathlib/pull/15482) data/list/basic: last_reverse 
+[PR #15139](https://github.com/leanprover-community/mathlib/pull/15139) data/list/basic: nth_le_enum 
+[PR #14777](https://github.com/leanprover-community/mathlib/pull/14777) data/list/basic: add filter_map_join 
+[PR #15473](https://github.com/leanprover-community/mathlib/pull/15473) data/list/infix: drop_while and take_while suf/prefix 
+[PR #15433](https://github.com/leanprover-community/mathlib/pull/15433) data/list/of_fn: lemmas to turn quantifiers over lists to quantifiers over tuples 
+[PR #15386](https://github.com/leanprover-community/mathlib/pull/15386) data/matrix/basic: Add `alg_equiv` and `linear_equiv` instances for transpose. 
+[PR #14991](https://github.com/leanprover-community/mathlib/pull/14991) data/matrix/notation: add `!![1, 2; 3, 4]` notation 
+[PR #15094](https://github.com/leanprover-community/mathlib/pull/15094) data/multiset/fintype: coercion from multiset to type 
+[PR #15457](https://github.com/leanprover-community/mathlib/pull/15457) data/nat/basic: add recursion principle `even_odd_rec` as a wrapper around `binary_rec` 
+[PR #15061](https://github.com/leanprover-community/mathlib/pull/15061) data/nat/basic: add `strong_sub_recursion` and `pincer_recursion` 
+[PR #15099](https://github.com/leanprover-community/mathlib/pull/15099) data/nat/basic: split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas 
+[PR #15031](https://github.com/leanprover-community/mathlib/pull/15031) data/nat/basic: add `mul_div_mul_comm_of_dvd_dvd` 
+[PR #15409](https://github.com/leanprover-community/mathlib/pull/15409) data/nat/bitwise: tweak `lxor` lemmas 
+[PR #15072](https://github.com/leanprover-community/mathlib/pull/15072) data/nat/choose/basic: Definition of `multichoose` and basic lemmas 
+[PR #15029](https://github.com/leanprover-community/mathlib/pull/15029) data/nat/enat: simple lemmas on `enat` 
+[PR #15767](https://github.com/leanprover-community/mathlib/pull/15767) data/nat/factorization/basic: add lemma `prime.factorization_self` 
+[PR #15277](https://github.com/leanprover-community/mathlib/pull/15277) data/nat/factorization/basic: golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` 
+[PR #15014](https://github.com/leanprover-community/mathlib/pull/15014) data/nat/factorization/basic: add lemma `factorization_eq_card_pow_dvd` 
+[PR #15539](https://github.com/leanprover-community/mathlib/pull/15539) data/nat/pairing: basic bounds on `mkpair` 
+[PR #15268](https://github.com/leanprover-community/mathlib/pull/15268) data/nat/parity: `nat.bit1_div_bit0` 
+[PR #15645](https://github.com/leanprover-community/mathlib/pull/15645) data/nat/totient: lemmas `totient_mul_of_prime_of_{not_}dvd` 
+[PR #15313](https://github.com/leanprover-community/mathlib/pull/15313) data/pfun: tooling to help reasoning about pfun domains 
+[PR #15588](https://github.com/leanprover-community/mathlib/pull/15588) data/pi/algebra: sum_elim lemmas 
+[PR #15508](https://github.com/leanprover-community/mathlib/pull/15508) data/pnat/basic: add lemmas, move `equiv.pnat_equiv_nat` 
+[PR #15183](https://github.com/leanprover-community/mathlib/pull/15183) data/pnat/basic: `succ` as an order isomorphism between `ℕ` and `ℕ+` 
+[PR #15199](https://github.com/leanprover-community/mathlib/pull/15199) data/polynomial/degree/definitions: redefine `polynomial.degree` as `p.support.max` 
+[PR #15522](https://github.com/leanprover-community/mathlib/pull/15522) data/polynomial/degree/lemmas: three lemmas on nat_degrees, bits and neg 
+[PR #14741](https://github.com/leanprover-community/mathlib/pull/14741) data/polynomial/erase_lead: Characterization of polynomials of fixed support 
+[PR #15225](https://github.com/leanprover-community/mathlib/pull/15225) data/polynomial/laurent: define `degree` and some API 
+[PR #15318](https://github.com/leanprover-community/mathlib/pull/15318) data/polynomial/unit_trinomial: Irreducibility of X^n-X-1 
+[PR #14914](https://github.com/leanprover-community/mathlib/pull/14914) data/polynomial/unit_trinomial: An irreducibility criterion for unit trinomials 
+[PR #15148](https://github.com/leanprover-community/mathlib/pull/15148) data/quot: `is_equiv` instance for quotient equivalence 
+[PR #15101](https://github.com/leanprover-community/mathlib/pull/15101) data/rat/defs: add denominator as pnat 
+[PR #15575](https://github.com/leanprover-community/mathlib/pull/15575) data/real/basic: add a repr showing an underlying cauchy sequence 
+[PR #15483](https://github.com/leanprover-community/mathlib/pull/15483) data/real/{e,}nnreal: images and preimages of `ord_connected` sets 
+[PR #14970](https://github.com/leanprover-community/mathlib/pull/14970) data/set/basic,order/filter/basic: add semiconj lemmas about images and maps 
+[PR #15671](https://github.com/leanprover-community/mathlib/pull/15671) data/set/countable: add `iff` versions of some lemmas 
+[PR #15415](https://github.com/leanprover-community/mathlib/pull/15415) data/set/countable: protect lemmas 
+[PR #15444](https://github.com/leanprover-community/mathlib/pull/15444) data/set/finite: set.finite.induction_on' 
+[PR #15177](https://github.com/leanprover-community/mathlib/pull/15177) data/set/finite: add `multiset.finite_to_set` 
+[PR #15605](https://github.com/leanprover-community/mathlib/pull/15605) data/set/function: add lemmas about `set.restrict` 
+[PR #15608](https://github.com/leanprover-community/mathlib/pull/15608) data/set/intervals: add lemmas 
+[PR #14928](https://github.com/leanprover-community/mathlib/pull/14928) data/set/pointwise: `list` and `multiset` versions of n-ary lemmas 
+[PR #15604](https://github.com/leanprover-community/mathlib/pull/15604) data/set/prod: add theorems about `λ x, (x, x)` 
+[PR #15652](https://github.com/leanprover-community/mathlib/pull/15652) data/sign: `left.sign_neg`, `right.sign_neg` 
+[PR #15358](https://github.com/leanprover-community/mathlib/pull/15358) data/sum/basic: `sum.lift_rel` is a subrelation of `sum.lex` 
+[PR #15370](https://github.com/leanprover-community/mathlib/pull/15370) data/sum/order: `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` 
+[PR #15192](https://github.com/leanprover-community/mathlib/pull/15192) data/sym/basic: combinatorial equivalence for `sym (option α) n.succ` 
+[PR #11162](https://github.com/leanprover-community/mathlib/pull/11162) data/sym/card: Prove stars and bars 
+[PR #15383](https://github.com/leanprover-community/mathlib/pull/15383) data/vector/basic: make the recursor work with `induction _ using` syntax 
+[PR #15154](https://github.com/leanprover-community/mathlib/pull/15154) data/vector/mem: Lemmas about membership in a vector 
+[PR #15493](https://github.com/leanprover-community/mathlib/pull/15493) data/{finset,set}/basic: `insert a s = s ↔ a ∈ s` 
+[PR #15478](https://github.com/leanprover-community/mathlib/pull/15478) data/{pi, prod}: add missing `has_pow` instances for `pi` type 
+[PR #15724](https://github.com/leanprover-community/mathlib/pull/15724) field_theory/adjoin: A compositum of algebraic extensions is algebraic 
+[PR #15426](https://github.com/leanprover-community/mathlib/pull/15426) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version 
+[PR #15518](https://github.com/leanprover-community/mathlib/pull/15518) field_theory/adjoin: `intermediate_field.exists_finset_of_mem_supr` 
+[PR #15438](https://github.com/leanprover-community/mathlib/pull/15438) field_theory/adjoin: Compact elements of `intermediate_field` 
+[PR #15420](https://github.com/leanprover-community/mathlib/pull/15420) field_theory/adjoin: `F⟮α⟯ ≤ K ↔ α ∈ K` 
+[PR #15339](https://github.com/leanprover-community/mathlib/pull/15339) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional 
+[PR #15659](https://github.com/leanprover-community/mathlib/pull/15659) field_theory/intermediate_field: Produce an intermediate field from a subalgebra satisfying `is_field`. 
+[PR #15188](https://github.com/leanprover-community/mathlib/pull/15188) field_theory/intermediate_field: `dsimp` lemma 
+[PR #15303](https://github.com/leanprover-community/mathlib/pull/15303) field_theory/tower: if `L / K / F` is finite, so is `K / F` 
+[PR #15021](https://github.com/leanprover-community/mathlib/pull/15021) geometry/euclidean/basic: `continuous_at_angle` 
+[PR #15463](https://github.com/leanprover-community/mathlib/pull/15463) geometry/euclidean/oriented_angle: `continuous_at_oangle` 
+[PR #15560](https://github.com/leanprover-community/mathlib/pull/15560) geometry/manifold: generalize some lemmas from `smooth` to `cont_mdiff` 
+[PR #15116](https://github.com/leanprover-community/mathlib/pull/15116) geometry/manifold/local_invariant_properties: simplify definitions and proofs 
+[PR #15437](https://github.com/leanprover-community/mathlib/pull/15437) geometry/manifold/metrizable: metrizability of a manifold 
+[PR #15314](https://github.com/leanprover-community/mathlib/pull/15314) geometry/manifold|topology: add simps and ext attributes 
+[PR #14182](https://github.com/leanprover-community/mathlib/pull/14182) group_theory/complement: transversal for the transfer homomorphism 
+[PR #15402](https://github.com/leanprover-community/mathlib/pull/15402) group_theory/finite_abelian: a finitely generated torsion abelian group is finite 
+[PR #15239](https://github.com/leanprover-community/mathlib/pull/15239) group_theory/group_action/option: Scalar action on an option 
+[PR #15050](https://github.com/leanprover-community/mathlib/pull/15050) group_theory/group_action/sub_mul_action: add the pointwise monoid structure 
+[PR #8632](https://github.com/leanprover-community/mathlib/pull/8632) group_theory/p_group: Groups of order p^2 are commutative 
+[PR #15052](https://github.com/leanprover-community/mathlib/pull/15052) group_theory/submonoid/pointwise: add the pointwise monoid structure on `add_submonoid` 
+[PR #13945](https://github.com/leanprover-community/mathlib/pull/13945) group_theory/subsemigroup/membership: add membership criteria for subsemigroups 
+[PR #14739](https://github.com/leanprover-community/mathlib/pull/14739) information_theory/hamming: add Hamming distance and norm 
+[PR #15603](https://github.com/leanprover-community/mathlib/pull/15603) integration: elementary version of FTC-1 
+[PR #15587](https://github.com/leanprover-community/mathlib/pull/15587) linear_algebra: lemmas on associatedness of determinants of linear maps 
+[PR #15119](https://github.com/leanprover-community/mathlib/pull/15119) linear_algebra: basis on R × R, and relation between matrices and linear maps in this basis  
+[PR #14714](https://github.com/leanprover-community/mathlib/pull/14714) linear_algebra/*: add lemma `linear_independent.finite_of_is_noetherian` 
+[PR #12140](https://github.com/leanprover-community/mathlib/pull/12140) linear_algebra/annihilating_polynomial: add definition of annihilating ideal and show minpoly generates in field case 
+[PR #14883](https://github.com/leanprover-community/mathlib/pull/14883) linear_algebra/basis: shows the lattice of submodules of a module over a division ring is atomistic 
+[PR #14790](https://github.com/leanprover-community/mathlib/pull/14790) linear_algebra/clifford_algebra/even: Universal property and isomorphisms for the even subalgebra 
+[PR #15558](https://github.com/leanprover-community/mathlib/pull/15558) linear_algebra/finite_dimensional: One-dimensional iff principal 
+[PR #15531](https://github.com/leanprover-community/mathlib/pull/15531) linear_algebra/linear_pmap: more lemmas about the graph 
+[PR #14922](https://github.com/leanprover-community/mathlib/pull/14922) linear_algebra/linear_pmap: construct a `linear_pmap` from its graph 
+[PR #14794](https://github.com/leanprover-community/mathlib/pull/14794) linear_algebra/matrix: inner prod of matrix 
+[PR #15459](https://github.com/leanprover-community/mathlib/pull/15459) linear_algebra/matrix/charpoly: Coefficients of the characteristic polynomial falls in the ideal power. 
+[PR #15391](https://github.com/leanprover-community/mathlib/pull/15391) linear_algebra/projective_space/subspace: defines subspaces of a projective space 
+[PR #14542](https://github.com/leanprover-community/mathlib/pull/14542) linear_algebra/projectivization/independence: defines (in)dependence of points in projective space 
+[PR #15628](https://github.com/leanprover-community/mathlib/pull/15628) linear_algebra/tensor_product: add id_apply and comp_apply for ltensor and rtensor 
+[PR #15209](https://github.com/leanprover-community/mathlib/pull/15209) linear_algebra/unitary_group: better constructor 
+[PR #15524](https://github.com/leanprover-community/mathlib/pull/15524) logic/encodable/basic: an encodable type is countable 
+[PR #15611](https://github.com/leanprover-community/mathlib/pull/15611) logic/equiv/local_equiv: add 2 lemmas 
+[PR #15176](https://github.com/leanprover-community/mathlib/pull/15176) logic/equiv/set: define `equiv.set.pi` 
+[PR #15574](https://github.com/leanprover-community/mathlib/pull/15574) logic/nonempty: `pi.nonempty` instance 
+[PR #15307](https://github.com/leanprover-community/mathlib/pull/15307) measure_theory/constructions/borel_space: the set of points for which a measurable sequence of functions converges is measurable 
+[PR #14424](https://github.com/leanprover-community/mathlib/pull/14424) measure_theory/constructions/prod: The layercake integral. 
+[PR #15422](https://github.com/leanprover-community/mathlib/pull/15422) measure_theory/function/conditional_expecation: conditional expectation of a function to a independent sigma-algebra  
+[PR #15274](https://github.com/leanprover-community/mathlib/pull/15274) measure_theory/function/conditional_expectation: pull-out property of the conditional expectation 
+[PR #15024](https://github.com/leanprover-community/mathlib/pull/15024) measure_theory/function/conditional_expectation: monotonicity of the conditional expectation 
+[PR #15378](https://github.com/leanprover-community/mathlib/pull/15378) measure_theory/function/uniform_integrable: conditional expectations form a uniformly integrable class 
+[PR #15120](https://github.com/leanprover-community/mathlib/pull/15120) measure_theory/group/measure: a product of Haar measures is a Haar measure 
+[PR #15423](https://github.com/leanprover-community/mathlib/pull/15423) measure_theory/integral: generalize some integral properties to set_to_fun 
+[PR #13885](https://github.com/leanprover-community/mathlib/pull/13885) measure_theory/integral: Circle integral transform 
+[PR #15344](https://github.com/leanprover-community/mathlib/pull/15344) measure_theory/integral/set_integral: add `set_integral_indicator` 
+[PR #15342](https://github.com/leanprover-community/mathlib/pull/15342) measure_theory/measurable_space_def: add `generate_from_induction` 
+[PR #15528](https://github.com/leanprover-community/mathlib/pull/15528) measure_theory/measure/finite_measure_weak_convergence: Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. 
+[PR #15205](https://github.com/leanprover-community/mathlib/pull/15205) measure_theory/measure/finite_measure_weak_convergence: Add some missing API lemmas. 
+[PR #15343](https://github.com/leanprover-community/mathlib/pull/15343) measure_theory/measure/measure_space: generalize measure.comap 
+[PR #15066](https://github.com/leanprover-community/mathlib/pull/15066) measure_theory/pmf: lawful monad instance for probability mass function monad 
+[PR #8002](https://github.com/leanprover-community/mathlib/pull/8002) number_theory: Bertrand's postulate, slightly different approach 
+[PR #15315](https://github.com/leanprover-community/mathlib/pull/15315) number_theory: degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` 
+[PR #15418](https://github.com/leanprover-community/mathlib/pull/15418) number_theory/legendre_symbol/*: redefine quadratic characters as `mul_char`s 
+[PR #15499](https://github.com/leanprover-community/mathlib/pull/15499) number_theory/legendre_symbol/add_character: add file introducing additive characters 
+[PR #15007](https://github.com/leanprover-community/mathlib/pull/15007) number_theory/slash_actions: Slash actions class for modular forms 
+[PR #14717](https://github.com/leanprover-community/mathlib/pull/14717) number_theory/wilson: add Wilson's Theorem 
+[PR #15149](https://github.com/leanprover-community/mathlib/pull/15149) order/basic: a symmetric relation implies equality when it implies less-equal 
+[PR #15606](https://github.com/leanprover-community/mathlib/pull/15606) order/boolean_algebra: A bounded generalized boolean algebra is a boolean algebra 
+[PR #15278](https://github.com/leanprover-community/mathlib/pull/15278) order/bounded_order: `is_well_order` instances for `with_top` and `with_bot` 
+[PR #15636](https://github.com/leanprover-community/mathlib/pull/15636) order/bounded_order: an order is either an `order_bot` or a `no_bot_order` 
+[PR #15341](https://github.com/leanprover-community/mathlib/pull/15341) order/bounded_order: two lemmas about the interaction between monotonicity and map with_bot/top 
+[PR #15357](https://github.com/leanprover-community/mathlib/pull/15357) order/bounded_order: `subrelation r s ↔ r ≤ s` 
+[PR #14195](https://github.com/leanprover-community/mathlib/pull/14195) order/bounded_order: Codisjointness 
+[PR #15665](https://github.com/leanprover-community/mathlib/pull/15665) order/compare: general cleanup 
+[PR #15340](https://github.com/leanprover-community/mathlib/pull/15340) order/complete_boolean_algebra: A frame is distributive 
+[PR #15237](https://github.com/leanprover-community/mathlib/pull/15237) order/filter: add `map_neg_at_top`, change some assumptions 
+[PR #15632](https://github.com/leanprover-community/mathlib/pull/15632) order/filter/*: `filter.pi` is countably generated 
+[PR #15630](https://github.com/leanprover-community/mathlib/pull/15630) order/filter/bases: lemmas about bases of product filters 
+[PR #15661](https://github.com/leanprover-community/mathlib/pull/15661) order/filter/basic: add `filter.has_basis.bInter_mem` 
+[PR #15128](https://github.com/leanprover-community/mathlib/pull/15128) order/filter/basic: add `map_le_map` and `map_injective` 
+[PR #15187](https://github.com/leanprover-community/mathlib/pull/15187) order/filter/ultrafilter: `pure`, `map`, and `comap` lemmas 
+[PR #15432](https://github.com/leanprover-community/mathlib/pull/15432) order/hom/basic: `order_iso` of `rel_iso (<) (<)` 
+[PR #15182](https://github.com/leanprover-community/mathlib/pull/15182) order/hom/basic: `order_iso` to `rel_iso (<) (<)` 
+[PR #15375](https://github.com/leanprover-community/mathlib/pull/15375) order/initial_seg: Initial/principal segment from empty type 
+[PR #15374](https://github.com/leanprover-community/mathlib/pull/15374) order/initial_seg: remove `nolint` from `initial_seg` 
+[PR #15439](https://github.com/leanprover-community/mathlib/pull/15439) order/lattice: Congruence lemmas for `⊔` and `⊓` 
+[PR #14789](https://github.com/leanprover-community/mathlib/pull/14789) order/lattice, data/set: some helper lemmas 
+[PR #15136](https://github.com/leanprover-community/mathlib/pull/15136) order/lattice, order/lattice_intervals: coe inf/sup lemmas 
+[PR #14733](https://github.com/leanprover-community/mathlib/pull/14733) order/locally_finite: make `fintype.to_locally_finite_order` computable 
+[PR #11602](https://github.com/leanprover-community/mathlib/pull/11602) order/modular_lattice: Semimodular lattices 
+[PR #15073](https://github.com/leanprover-community/mathlib/pull/15073) order/order_iso_nat: generalize `well_founded.monotone_chain_condition` to preorders 
+[PR #15350](https://github.com/leanprover-community/mathlib/pull/15350) order/partition/finpartition: Bound size of a bit of `finpartition.atomise` 
+[PR #15430](https://github.com/leanprover-community/mathlib/pull/15430) order/rel_iso: add lemmas on `rel_iso.cast` 
+[PR #15372](https://github.com/leanprover-community/mathlib/pull/15372) order/rel_iso: relation embedding from empty type 
+[PR #14760](https://github.com/leanprover-community/mathlib/pull/14760) order/rel_iso: two reflexive/irreflexive relations on a unique type are isomorphic 
+[PR #15144](https://github.com/leanprover-community/mathlib/pull/15144) order/rel_iso: add `rel_iso.cast` 
+[PR #15016](https://github.com/leanprover-community/mathlib/pull/15016) order/succ_pred: expand API on `with_bot` and `with_top` 
+[PR #15567](https://github.com/leanprover-community/mathlib/pull/15567) order/succ_pred/basic: `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related 
+[PR #15536](https://github.com/leanprover-community/mathlib/pull/15536) order/succ_pred/basic: `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses 
+[PR #15001](https://github.com/leanprover-community/mathlib/pull/15001) order/succ_pred/limit: Successor and predecessor limits 
+[PR #15581](https://github.com/leanprover-community/mathlib/pull/15581) order/upper_lower: Upper closure of a set 
+[PR #15399](https://github.com/leanprover-community/mathlib/pull/15399) order/well_founded: typeclasses for well-founded `<` and `>` 
+[PR #15266](https://github.com/leanprover-community/mathlib/pull/15266) order/well_founded_set: any relation is well-founded on `Ø` 
+[PR #15678](https://github.com/leanprover-community/mathlib/pull/15678) probability/density: probability of event in uniform distribution 
+[PR #15131](https://github.com/leanprover-community/mathlib/pull/15131) probability/independence: two tuples indexed by disjoint subsets of an independent family of r.v. are independent 
+[PR #14909](https://github.com/leanprover-community/mathlib/pull/14909) probability/martingale: the discrete stochastic integral of a submartingale is a submartingale 
+[PR #14737](https://github.com/leanprover-community/mathlib/pull/14737) probability/martingale: Doob's maximal inequality 
+[PR #14932](https://github.com/leanprover-community/mathlib/pull/14932) probability/martingale: positive part of a submartingale is also a submartingale 
+[PR #15140](https://github.com/leanprover-community/mathlib/pull/15140) probability/moments: mgf/cgf of a sum of independent random variables 
+[PR #15129](https://github.com/leanprover-community/mathlib/pull/15129) probability/moments: Chernoff bound on the upper/lower tail of a real random variable 
+[PR #15392](https://github.com/leanprover-community/mathlib/pull/15392) probability/strong_law: Lp version of the strong law of large numbers 
+[PR #14331](https://github.com/leanprover-community/mathlib/pull/14331) representation_theory/Action: mapping by a monoidal functor 
+[PR #13713](https://github.com/leanprover-community/mathlib/pull/13713) representation_theory/Rep: Rep k G ≌ Module (monoid_algebra k G) 
+[PR #15084](https://github.com/leanprover-community/mathlib/pull/15084) representation_theory/character: formula for the dimension of the invariants in terms of the character 
+[PR #14308](https://github.com/leanprover-community/mathlib/pull/14308) representation_theory/monoid_algebra_basis: add some API for `k[G^n]` 
+[PR #15243](https://github.com/leanprover-community/mathlib/pull/15243) ring_theory: Formally étale/smooth/unramified morphisms are stable under base change. 
+[PR #14348](https://github.com/leanprover-community/mathlib/pull/14348) ring_theory: the Ore localization of a ring 
+[PR #15381](https://github.com/leanprover-community/mathlib/pull/15381) ring_theory: the integral closure `C` of `A` is Noetherian over `A` 
+[PR #14966](https://github.com/leanprover-community/mathlib/pull/14966) ring_theory: Basic framework for classes of ring homomorphisms 
+[PR #15064](https://github.com/leanprover-community/mathlib/pull/15064) ring_theory: Some missing lemmas 
+[PR #15333](https://github.com/leanprover-community/mathlib/pull/15333) ring_theory/I_filtration: I-filtrations of modules. 
+[PR #14981](https://github.com/leanprover-community/mathlib/pull/14981) ring_theory/adjoin_root: add lemmas for GCD domains 
+[PR #15586](https://github.com/leanprover-community/mathlib/pull/15586) ring_theory/algebraic: `is_algebraic_algebra_map_iff` 
+[PR #15424](https://github.com/leanprover-community/mathlib/pull/15424) ring_theory/bezout: Bezout domains are integrally closed 
+[PR #15091](https://github.com/leanprover-community/mathlib/pull/15091) ring_theory/bezout: Define Bézout rings. 
+[PR #11053](https://github.com/leanprover-community/mathlib/pull/11053) ring_theory/dedekind_domain: If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape 
+[PR #15244](https://github.com/leanprover-community/mathlib/pull/15244) ring_theory/derivation: Derivations into square-zero ideals corresponds to liftings.  
+[PR #15242](https://github.com/leanprover-community/mathlib/pull/15242) ring_theory/etale: Formally étale morphisms. 
+[PR #15264](https://github.com/leanprover-community/mathlib/pull/15264) ring_theory/graded_algebra/basic: add lemma `proj_homogeneous_mul` 
+[PR #15460](https://github.com/leanprover-community/mathlib/pull/15460) ring_theory/ideal/operations: A variant of `finsupp.total` for ideals. 
+[PR #12812](https://github.com/leanprover-community/mathlib/pull/12812) ring_theory/integrally_closed: if x is in Frac R such that x^n is in R then x is in R 
+[PR #15404](https://github.com/leanprover-community/mathlib/pull/15404) ring_theory/localization/basic: section of localisation of non-zero is non-zero 
+[PR #15261](https://github.com/leanprover-community/mathlib/pull/15261) ring_theory/localization/basic: add `mk_sum` 
+[PR #15561](https://github.com/leanprover-community/mathlib/pull/15561) ring_theory/noetherian: Finitely generated idempotent ideal is principal. 
+[PR #15397](https://github.com/leanprover-community/mathlib/pull/15397) ring_theory/power_series/basic: Add `rescale_X` 
+[PR #15287](https://github.com/leanprover-community/mathlib/pull/15287) ring_theory/power_series/well_known: Coefficients of sin and cos 
+[PR #15089](https://github.com/leanprover-community/mathlib/pull/15089) ring_theory/rees_algebra: Define the Rees algebra of an ideal. 
+[PR #15427](https://github.com/leanprover-community/mathlib/pull/15427) ring_theory/ring_hom/finite: Finite ring morphisms are stable under base change 
+[PR #15379](https://github.com/leanprover-community/mathlib/pull/15379) ring_theory/ring_hom/finite: Finite type is a local property 
+[PR #15512](https://github.com/leanprover-community/mathlib/pull/15512) ring_theory/tensor_product: A predicate for being the tensor product. 
+[PR #15241](https://github.com/leanprover-community/mathlib/pull/15241) ring_theory/tensor_product: `A`-algebra structure on `A' ⊗[R] B`. 
+[PR #15093](https://github.com/leanprover-community/mathlib/pull/15093) ring_theory/valuation: Properties of valuation rings. 
+[PR #14896](https://github.com/leanprover-community/mathlib/pull/14896) set/intervals/monotone: add some monotonicity lemmas 
+[PR #14989](https://github.com/leanprover-community/mathlib/pull/14989) set_theory/cardinal/ordinal: basic properties on Beth numbers 
+[PR #15198](https://github.com/leanprover-community/mathlib/pull/15198) set_theory/cardinal/ordinal: cardinality of `α →₀ β` 
+[PR #15367](https://github.com/leanprover-community/mathlib/pull/15367) set_theory/game/nim: make the file `noncomputable theory` 
+[PR #14780](https://github.com/leanprover-community/mathlib/pull/14780) set_theory/game/ordinal: lemmas on `0.to_pgame` and `1.to_pgame` 
+[PR #15255](https://github.com/leanprover-community/mathlib/pull/15255) set_theory/game/pgame: strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` 
+[PR #15256](https://github.com/leanprover-community/mathlib/pull/15256) set_theory/game/pgame: `is_option (-x) (-y) ↔ is_option x y` 
+[PR #15254](https://github.com/leanprover-community/mathlib/pull/15254) set_theory/game/pgame: add `equiv.comm` 
+[PR #15533](https://github.com/leanprover-community/mathlib/pull/15533) set_theory/ordinal/arithmetic: `pred 0 = 0` 
+[PR #15447](https://github.com/leanprover-community/mathlib/pull/15447) set_theory/ordinal/arithmetic: more log lemmas 
+[PR #15193](https://github.com/leanprover-community/mathlib/pull/15193) set_theory/ordinal/arithmetic: tweak `type_add` and `type_mul` 
+[PR #15174](https://github.com/leanprover-community/mathlib/pull/15174) set_theory/ordinal/arithmetic: tweak theorems about `0` and `1` 
+[PR #15348](https://github.com/leanprover-community/mathlib/pull/15348) set_theory/ordinal/basic: dot notation lemmas + golf 
+[PR #15152](https://github.com/leanprover-community/mathlib/pull/15152) set_theory/ordinal/basic: add `gc_ord_card` and `gci_ord_card` 
+[PR #15194](https://github.com/leanprover-community/mathlib/pull/15194) set_theory/ordinal/basic: mark `type_fintype` as `simp` 
+[PR #15178](https://github.com/leanprover-community/mathlib/pull/15178) set_theory/ordinal/basic: order type of naturals is `ω` 
+[PR #15146](https://github.com/leanprover-community/mathlib/pull/15146) set_theory/ordinal/basic: basic lemmas on `ordinal.lift`  
+[PR #15320](https://github.com/leanprover-community/mathlib/pull/15320) set_theory/zfc: ZFC sets are small types 
+[PR #15223](https://github.com/leanprover-community/mathlib/pull/15223) set_theory/zfc: `Ø ⊆ x` 
+[PR #15213](https://github.com/leanprover-community/mathlib/pull/15213) set_theory/zfc: `∈` is well-founded 
+[PR #15324](https://github.com/leanprover-community/mathlib/pull/15324) set_theory/zfc: more `quotient` lemmas 
+[PR #15214](https://github.com/leanprover-community/mathlib/pull/15214) set_theory/zfc: simp lemmas for `arity` and `const` 
+[PR #15211](https://github.com/leanprover-community/mathlib/pull/15211) set_theory/zfc: basic lemmas on `pSet.equiv` 
+[PR #15545](https://github.com/leanprover-community/mathlib/pull/15545) set_theory/zfc/basic: `inj` lemmas 
+[PR #15544](https://github.com/leanprover-community/mathlib/pull/15544) set_theory/zfc/basic: `∈` is well-founded on classes 
+[PR #15573](https://github.com/leanprover-community/mathlib/pull/15573) set_theory/zfc/basic: `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` 
+[PR #15551](https://github.com/leanprover-community/mathlib/pull/15551) set_theory/zfc/basic: `⊆` is reflexive, transitive, antisymmetric 
+[PR #15549](https://github.com/leanprover-community/mathlib/pull/15549) set_theory/zfc/basic: add `refl`, `symm`, `trans` attributes to `equiv` lemmas 
+[PR #15548](https://github.com/leanprover-community/mathlib/pull/15548) set_theory/zfc/ordinal: more lemmas on transitive sets 
+[PR #15288](https://github.com/leanprover-community/mathlib/pull/15288) set_theory/zfc/ordinal: transitive sets 
+[PR #15498](https://github.com/leanprover-community/mathlib/pull/15498) tactic/attribute: add `expand_exists` 
+[PR #14762](https://github.com/leanprover-community/mathlib/pull/14762) tactic/compute_degree + test/compute_degree: introduce a tactic for proving `f.(nat_)degree ≤ d` 
+[PR #14532](https://github.com/leanprover-community/mathlib/pull/14532) tactic/congrm: add "function underscores" to `congrm` 
+[PR #15502](https://github.com/leanprover-community/mathlib/pull/15502) tactic/ext: don't remove attr 
+[PR #15319](https://github.com/leanprover-community/mathlib/pull/15319) tactic/linear_combination: allow linear_combination to leave goal open 
+[PR #15284](https://github.com/leanprover-community/mathlib/pull/15284) tactic/linear_combination: add parser for `h / a` 
+[PR #15202](https://github.com/leanprover-community/mathlib/pull/15202) tactic/lint: add a linter for `[fintype _]` assumptions 
+[PR #14878](https://github.com/leanprover-community/mathlib/pull/14878) tactic/polyrith: a tactic using Sage to solve polynomial equalities with hypotheses 
+[PR #15618](https://github.com/leanprover-community/mathlib/pull/15618) tactic/positivity: a tactic for proving positivity/nonnegativity 
+[PR #15728](https://github.com/leanprover-community/mathlib/pull/15728) test/polyrith: better formatting for generated tests 
+[PR #15641](https://github.com/leanprover-community/mathlib/pull/15641) tooplogy/metric_space/hausdorff_distance: add lemmas about `thickening` 
+[PR #15102](https://github.com/leanprover-community/mathlib/pull/15102) topology: basic simplification lemmas for `continuous_map`s 
+[PR #14806](https://github.com/leanprover-community/mathlib/pull/14806) topology/algebra/filter_basis: add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group 
+[PR #15157](https://github.com/leanprover-community/mathlib/pull/15157) topology/algebra/infinite_sum: Double sum is equal to a single value 
+[PR #15610](https://github.com/leanprover-community/mathlib/pull/15610) topology/algebra/module/finite_dimension: add 2 simp lemmas 
+[PR #15022](https://github.com/leanprover-community/mathlib/pull/15022) topology/algebra/order: ⁻¹ continuous for linear ordered fields 
+[PR #14889](https://github.com/leanprover-community/mathlib/pull/14889) topology/algebra/uniform_group: `uniform_group` is preserved by Inf and comap 
+[PR #15653](https://github.com/leanprover-community/mathlib/pull/15653) topology/basic: add lemmas about `filter.lift' _ closure` 
+[PR #15580](https://github.com/leanprover-community/mathlib/pull/15580) topology/basic: a condition implying that a sequence of functions locally stabilizes 
+[PR #15485](https://github.com/leanprover-community/mathlib/pull/15485) topology/basic: add 2 lemmas about `locally_finite` families 
+[PR #14036](https://github.com/leanprover-community/mathlib/pull/14036) topology/continuous_function: Any T0 space embeds in a product of copies of the Sierpinski space 
+[PR #14724](https://github.com/leanprover-community/mathlib/pull/14724) topology/homotopy: define nth homotopy group πₙ (without the group instance) 
+[PR #15593](https://github.com/leanprover-community/mathlib/pull/15593) topology/instances/ennreal: add `continuous(_on).ennreal_mul` 
+[PR #15446](https://github.com/leanprover-community/mathlib/pull/15446) topology/instances/nnreal: add `can_lift C(X, ℝ) C(X, ℝ≥0)` 
+[PR #15311](https://github.com/leanprover-community/mathlib/pull/15311) topology/local_homeomorph: "injectivity" local_homeomorph.prod 
+[PR #15612](https://github.com/leanprover-community/mathlib/pull/15612) topology/maps: add 2 lemmas, `open function` 
+[PR #15165](https://github.com/leanprover-community/mathlib/pull/15165) topology/maps: more `iff` lemmas 
+[PR #14926](https://github.com/leanprover-community/mathlib/pull/14926) topology/metric_space/hausdorff_distance: Thickening a compact inside an open 
+[PR #15591](https://github.com/leanprover-community/mathlib/pull/15591) topology/metric_space/isometry: use namespace, add lemmas 
+[PR #15634](https://github.com/leanprover-community/mathlib/pull/15634) topology/metric_space/lipschitz: add several lemmas 
+[PR #14965](https://github.com/leanprover-community/mathlib/pull/14965) topology/noetherian_space: Noetherian spaces 
+[PR #15617](https://github.com/leanprover-community/mathlib/pull/15617) topology/order: upgrade some lemmas to `iff`s 
+[PR #15490](https://github.com/leanprover-community/mathlib/pull/15490) topology/partition_of_unity: local to global 
+[PR #15635](https://github.com/leanprover-community/mathlib/pull/15635) topology/separation: add `disjoint_nhds_nhds` 
+[PR #15043](https://github.com/leanprover-community/mathlib/pull/15043) topology/separation: `separation_quotient α` is a T₀ space 
+[PR #15338](https://github.com/leanprover-community/mathlib/pull/15338) topology/sets/closeds: The coframe of closed sets 
+[PR #15118](https://github.com/leanprover-community/mathlib/pull/15118) topology/sets/compacts: prod constructions 
+[PR #15707](https://github.com/leanprover-community/mathlib/pull/15707) topology/subset_properties: `locally_compact_space` instance for `Π` types 
+[PR #15484](https://github.com/leanprover-community/mathlib/pull/15484) topology/support: add lemmas, fix a name 
+[PR #15346](https://github.com/leanprover-community/mathlib/pull/15346) topology/support: tsupport of product is a subset of tsupport 
+[PR #14892](https://github.com/leanprover-community/mathlib/pull/14892) topology/uniform_space/basic: uniform continuity from/to an infimum of uniform spaces 

From 683efae8394da9cd8c59273dd09c4dd8b5649905 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 3 Aug 2022 01:03:56 +0200
Subject: [PATCH 2/5] more tests

---
 posts/month-in-mathlib-jul-2022.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/posts/month-in-mathlib-jul-2022.md b/posts/month-in-mathlib-jul-2022.md
index ee832cac..ba5d90f3 100644
--- a/posts/month-in-mathlib-jul-2022.md
+++ b/posts/month-in-mathlib-jul-2022.md
@@ -11,8 +11,9 @@ title: This month in mathlib (Jul 2022)
 type: text
 ---
 
-[PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) *: add lemmas about sigma types 
-[PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) */partition_of_unity: more lemmas based on the partition of unity 
+* [PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) *: add lemmas about sigma types 
+* [PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) */partition_of_unity: more lemmas based on the partition of unity 
+
 [PR #15744](https://github.com/leanprover-community/mathlib/pull/15744) algebra/algebra/subalgebra/basic: Swap arguments of `map` and `comap` 
 [PR #15556](https://github.com/leanprover-community/mathlib/pull/15556) algebra/big_operators: add lemmas about sum of disjoint multiset 
 [PR #15095](https://github.com/leanprover-community/mathlib/pull/15095) algebra/category: forgetful functors from modules reflect limits 

From 3a031cce6d4f49ad1cbbdf511d735ca6ef91b1b0 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 3 Aug 2022 01:15:16 +0200
Subject: [PATCH 3/5] added indentation

---
 get_month.py                       |   6 +-
 posts/month-in-mathlib-jul-2022.md | 809 ++++++++++++++---------------
 2 files changed, 407 insertions(+), 408 deletions(-)

diff --git a/get_month.py b/get_month.py
index 42f8bf07..365de3a1 100644
--- a/get_month.py
+++ b/get_month.py
@@ -23,7 +23,7 @@ def extract_msg_title(title):
     start = title.index(')') # this is totally stupid, but some people forget the colon
     words = title.split()
     end = len(words[-1])
-    return title[start+2:-end].lstrip()
+    return title[start+2:-end].strip()
 
 class mathlib_commit():
     def __init__(self, commit):
@@ -55,7 +55,7 @@ def __init__(self, commit):
 
 sorted_commits = sorted(mathlib_commits, key=lambda commit: commit.folder)
 
-this_month_file = open("this_month_" + str(args.year) + "_" + monthnames_lc[args.month], "a")
+this_month_file = open("month-in-mathlib-" + monthnames_lc[args.month] + "_" + str(args.year) + ".md", "a")
 
 print("Number of commits: " + str(number_of_commits))
 
@@ -67,6 +67,6 @@ def __init__(self, commit):
 
 for commit in sorted_commits:
     if commit.feature:
-        print("[PR #" + commit.pr +
+        print("* [PR #" + commit.pr +
                 "](https://github.com/leanprover-community/mathlib/pull/" +
                 commit.pr + ")" + " " + commit.folder + ": " + commit.msg_title, file=this_month_file)
diff --git a/posts/month-in-mathlib-jul-2022.md b/posts/month-in-mathlib-jul-2022.md
index ba5d90f3..fc66f416 100644
--- a/posts/month-in-mathlib-jul-2022.md
+++ b/posts/month-in-mathlib-jul-2022.md
@@ -11,408 +11,407 @@ title: This month in mathlib (Jul 2022)
 type: text
 ---
 
-* [PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) *: add lemmas about sigma types 
-* [PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) */partition_of_unity: more lemmas based on the partition of unity 
-
-[PR #15744](https://github.com/leanprover-community/mathlib/pull/15744) algebra/algebra/subalgebra/basic: Swap arguments of `map` and `comap` 
-[PR #15556](https://github.com/leanprover-community/mathlib/pull/15556) algebra/big_operators: add lemmas about sum of disjoint multiset 
-[PR #15095](https://github.com/leanprover-community/mathlib/pull/15095) algebra/category: forgetful functors from modules reflect limits 
-[PR #15019](https://github.com/leanprover-community/mathlib/pull/15019) algebra/category/BoolRing: The equivalence between Boolean rings and Boolean algebras 
-[PR #15330](https://github.com/leanprover-community/mathlib/pull/15330) algebra/category/Group: The forgetful-units adjunction between `Group` and `Mon`. 
-[PR #14328](https://github.com/leanprover-community/mathlib/pull/14328) algebra/category/Module: upgrade `free : Type ⥤ Module R` to a monoidal functor 
-[PR #14720](https://github.com/leanprover-community/mathlib/pull/14720) algebra/category_theory/Group/epi_mono: about monomorphism and epimorphism in category of group 
-[PR #15654](https://github.com/leanprover-community/mathlib/pull/15654) algebra/direct_sum/decomposition: add an induction principle for `direct_sum.decomposition` class 
-[PR #15109](https://github.com/leanprover-community/mathlib/pull/15109) algebra/gcd_monoid: GCD domains are integrally closed. 
-[PR #15403](https://github.com/leanprover-community/mathlib/pull/15403) algebra/group/with_one: units of a group with zero is isomorphic to the group 
-[PR #14945](https://github.com/leanprover-community/mathlib/pull/14945) algebra/homology: homotopy equivalences are quasi-isomorphisms 
-[PR #11073](https://github.com/leanprover-community/mathlib/pull/11073) algebra/jordan: Introduce Jordan rings 
-[PR #14179](https://github.com/leanprover-community/mathlib/pull/14179) algebra/lie/cartan_subalgebra: characterise Cartan subalgebras as limiting values of upper central series 
-[PR #15675](https://github.com/leanprover-community/mathlib/pull/15675) algebra/lie/of_associative: add `commute.lie_eq` 
-[PR #15733](https://github.com/leanprover-community/mathlib/pull/15733) algebra/module: sub_mem_sup for modules over rings 
-[PR #12895](https://github.com/leanprover-community/mathlib/pull/12895) algebra/module: add injective module and Baer's criterion 
-[PR #15103](https://github.com/leanprover-community/mathlib/pull/15103) algebra/module/linear_map: use morphisms class for lemmas about linear [pre]images of `c • S` 
-[PR #14470](https://github.com/leanprover-community/mathlib/pull/14470) algebra/module/localized_module: construction of module localisation 
-[PR #15092](https://github.com/leanprover-community/mathlib/pull/15092) algebra/module/torsion: `R/I`-module structure on `M/IM`. 
-[PR #3292](https://github.com/leanprover-community/mathlib/pull/3292) algebra/order/complete_field: `conditionally_complete_linear_ordered_field`, aka the reals 
-[PR #15300](https://github.com/leanprover-community/mathlib/pull/15300) algebra/order/monoid: add lemmas `map_add` for `with_bot/top` 
-[PR #15458](https://github.com/leanprover-community/mathlib/pull/15458) algebra/order/monoid: add `one_lt_mul_iff`/`add_pos_iff` 
-[PR #15219](https://github.com/leanprover-community/mathlib/pull/15219) algebra/order/monoid: Add zero_le_three and zero_le_four 
-[PR #15267](https://github.com/leanprover-community/mathlib/pull/15267) algebra/order/monoid_lemmas: add `antitone`, `monotone_on`, and `antitone_on` lemmas 
-[PR #14761](https://github.com/leanprover-community/mathlib/pull/14761) algebra/order/monoid_lemmas_zero_lt: add some lemmas about typeclasses 
-[PR #14770](https://github.com/leanprover-community/mathlib/pull/14770) algebra/order/monoid_lemmas_zero_lt: add missing lemmas 
-[PR #15186](https://github.com/leanprover-community/mathlib/pull/15186) algebra/parity: more general odd.pos 
-[PR #15660](https://github.com/leanprover-community/mathlib/pull/15660) algebra/periodic: `fract_periodic` 
-[PR #13958](https://github.com/leanprover-community/mathlib/pull/13958) algebra/ring/{pi, prod, opposite}: add basic defs for non_unital_ring_hom 
-[PR #15291](https://github.com/leanprover-community/mathlib/pull/15291) algebraic_geometry: comap of surjective homomorphism is closed embedding 
-[PR #11649](https://github.com/leanprover-community/mathlib/pull/11649) algebraic_geometry: Intersection of affine open can be covered by common basic opens 
-[PR #14972](https://github.com/leanprover-community/mathlib/pull/14972) algebraic_geometry: Restriction of morphisms onto open sets of the target 
-[PR #15487](https://github.com/leanprover-community/mathlib/pull/15487) algebraic_geometry/AffineScheme: Affine communication lemma 
-[PR #15365](https://github.com/leanprover-community/mathlib/pull/15365) algebraic_geometry/EllipticCurve: simplify definition of discriminant 
-[PR #15436](https://github.com/leanprover-community/mathlib/pull/15436) algebraic_geometry/morphisms: Quasi-compact morphisms of schemes 
-[PR #14944](https://github.com/leanprover-community/mathlib/pull/14944) algebraic_geometry/morphisms: Basic framework for classes of morphisms between schemes 
-[PR #13397](https://github.com/leanprover-community/mathlib/pull/13397) algebraic_geometry/projective_spectrum: forward direction of homeomorphism between top_space of Proj and top_space of Spec 
-[PR #14588](https://github.com/leanprover-community/mathlib/pull/14588) algebraic_topology: alternating_coface_map_complex 
-[PR #15616](https://github.com/leanprover-community/mathlib/pull/15616) algebraic_topology/dold_kan: construction of idempotent endomorphisms 
-[PR #14044](https://github.com/leanprover-community/mathlib/pull/14044) algebraic_topology/dold_kan: technical lemmas about face maps 
-[PR #12788](https://github.com/leanprover-community/mathlib/pull/12788) algebraic_topology/fundamental_groupoid: Define simply connected spaces 
-[PR #15568](https://github.com/leanprover-community/mathlib/pull/15568) analysis/asymptotics: add `is_o*.of_pow` 
-[PR #15010](https://github.com/leanprover-community/mathlib/pull/15010) analysis/asymptotics/asymptotics: generalize, golf 
-[PR #15416](https://github.com/leanprover-community/mathlib/pull/15416) analysis/calculus: generalize `differentiable*.pow`, add `differentiable*.zpow` 
-[PR #15595](https://github.com/leanprover-community/mathlib/pull/15595) analysis/calculus/cont_diff: generalize `mul` lemmas to a normed algebra 
-[PR #15309](https://github.com/leanprover-community/mathlib/pull/15309) analysis/calculus/cont_diff: extra lemmas about cont_diff_within_at 
-[PR #15133](https://github.com/leanprover-community/mathlib/pull/15133) analysis/calculus/mean_value: remove assumption in strict_mono_on.strict_convex_on_of_deriv 
-[PR #15122](https://github.com/leanprover-community/mathlib/pull/15122) analysis/complex: equiv_real_prod_symm_apply 
-[PR #15364](https://github.com/leanprover-community/mathlib/pull/15364) analysis/complex/abs_max: add a version of the maximum modulus principle 
-[PR #15639](https://github.com/leanprover-community/mathlib/pull/15639) analysis/convex/cone: add inner_dual_cone_eq_Inter_inner_dual_cone_singleton 
-[PR #14821](https://github.com/leanprover-community/mathlib/pull/14821) analysis/convex/function: Variants of `convex_on.le_right_of_left_le` 
-[PR #15363](https://github.com/leanprover-community/mathlib/pull/15363) analysis/inner_product/calculus: [higher] differentiability to/from `euclidean_space` 
-[PR #15481](https://github.com/leanprover-community/mathlib/pull/15481) analysis/inner_product/pi_L2: a finite orthonormal family is a basis of its span 
-[PR #15540](https://github.com/leanprover-community/mathlib/pull/15540) analysis/inner_product_space: in finite dimension, hilbert basis = orthonormal basis 
-[PR #15055](https://github.com/leanprover-community/mathlib/pull/15055) analysis/inner_product_space: the Hellinger-Toeplitz theorem 
-[PR #15020](https://github.com/leanprover-community/mathlib/pull/15020) analysis/inner_product_space: add simple lemmas for the orthogonal complement 
-[PR #15514](https://github.com/leanprover-community/mathlib/pull/15514) analysis/inner_product_space/[pi_L2, l2_space]: compute inner product in a given [orthonormal, hilbert] basis 
-[PR #15577](https://github.com/leanprover-community/mathlib/pull/15577) analysis/inner_product_space/basic: `orthonormal` version of `linear_independent.coe_range` 
-[PR #15470](https://github.com/leanprover-community/mathlib/pull/15470) analysis/inner_product_space/positive: definition and basic facts about positive operators 
-[PR #14876](https://github.com/leanprover-community/mathlib/pull/14876) analysis/locally_convex/basic: a few lemmas about balanced sets 
-[PR #15124](https://github.com/leanprover-community/mathlib/pull/15124) analysis/locally_convex/with_seminorms: in a normed space, von Neumann bounded = metric bounded 
-[PR #15515](https://github.com/leanprover-community/mathlib/pull/15515) analysis/normed*: add instances and lemmas 
-[PR #15467](https://github.com/leanprover-community/mathlib/pull/15467) analysis/normed_space/compact_operator: definition and basic facts about compact operators 
-[PR #15650](https://github.com/leanprover-community/mathlib/pull/15650) analysis/normed_space/linear_isometry: add defs and lemmas 
-[PR #15471](https://github.com/leanprover-community/mathlib/pull/15471) analysis/normed_space/linear_isometry: `linear_equiv.of_eq` as a `linear_isometry_equiv` 
-[PR #15317](https://github.com/leanprover-community/mathlib/pull/15317) analysis/normed_space/lp_space: construct star structures on lp spaces 
-[PR #15086](https://github.com/leanprover-community/mathlib/pull/15086) analysis/normed_space/lp_space: normed_algebra structure 
-[PR #14104](https://github.com/leanprover-community/mathlib/pull/14104) analysis/normed_space/lp_space: add l_infinity ring instances 
-[PR #15578](https://github.com/leanprover-community/mathlib/pull/15578) analysis/normed_space/operator_norm: variant of `continuous_linear_equiv.has_sum` 
-[PR #15417](https://github.com/leanprover-community/mathlib/pull/15417) analysis/normed_space/operator_norm: add 2 new versions of `op_norm_le_*` 
-[PR #15173](https://github.com/leanprover-community/mathlib/pull/15173) analysis/normed_space/star/basic: make starₗᵢ apply to normed star groups 
-[PR #15125](https://github.com/leanprover-community/mathlib/pull/15125) analysis/special_functions/complex/arg: add complex.abs_eq_one_iff 
-[PR #14980](https://github.com/leanprover-community/mathlib/pull/14980) analysis/special_functions/complex/arg: `continuous_at_arg_coe_angle` 
-[PR #15506](https://github.com/leanprover-community/mathlib/pull/15506) analysis/special_functions/exp: add lemmas about `is_o`/`is_O`/`is_Theta` 
-[PR #15106](https://github.com/leanprover-community/mathlib/pull/15106) analysis/special_functions/gaussian: formula for gaussian integrals 
-[PR #15258](https://github.com/leanprover-community/mathlib/pull/15258) analysis/special_functions/polar_coord: define polar coordinates, polar change of variable formula in integrals 
-[PR #15164](https://github.com/leanprover-community/mathlib/pull/15164) analysis/special_functions/pow: drop an assumption in `is_o_log_rpow_rpow_at_top` 
-[PR #15002](https://github.com/leanprover-community/mathlib/pull/15002) analysis/special_functions/pow: Rational powers are dense 
-[PR #15651](https://github.com/leanprover-community/mathlib/pull/15651) analysis/special_functions/trigonometric/angle: equality of `cos` or `sin` 
-[PR #14988](https://github.com/leanprover-community/mathlib/pull/14988) analysis/special_functions/trigonometric/angle: equality of twice angles 
-[PR #15360](https://github.com/leanprover-community/mathlib/pull/15360) big_operators/fin: sum over elements of vector equal to `a` equals count `a` 
-[PR #14422](https://github.com/leanprover-community/mathlib/pull/14422) category_theory: construction of the localized category 
-[PR #14838](https://github.com/leanprover-community/mathlib/pull/14838) category_theory: a characterization of separating objects 
-[PR #14974](https://github.com/leanprover-community/mathlib/pull/14974) category_theory: full_of_surjective 
-[PR #15238](https://github.com/leanprover-community/mathlib/pull/15238) category_theory: a category with a small detecting set is well-powered 
-[PR #15377](https://github.com/leanprover-community/mathlib/pull/15377) category_theory: limits of essentially small indexing categories 
-[PR #14880](https://github.com/leanprover-community/mathlib/pull/14880) category_theory: (co)products and (co)separators 
-[PR #14026](https://github.com/leanprover-community/mathlib/pull/14026) category_theory: left-exact functors preserve finite limits 
-[PR #15121](https://github.com/leanprover-community/mathlib/pull/15121) category_theory/*/algebra: epi_of_epi and mono_of_mono 
-[PR #14581](https://github.com/leanprover-community/mathlib/pull/14581) category_theory/abelian/*: functors that preserve finite limits and colimits preserve exactness 
-[PR #14834](https://github.com/leanprover-community/mathlib/pull/14834) category_theory/endofunctor/algebra: Define coalgebras over an endofunctor and prove an equivalence 
-[PR #14829](https://github.com/leanprover-community/mathlib/pull/14829) category_theory/functor: preserving/reflecting monos/epis 
-[PR #14419](https://github.com/leanprover-community/mathlib/pull/14419) category_theory/limits: preserves biproducts if comparison is iso 
-[PR #14526](https://github.com/leanprover-community/mathlib/pull/14526) category_theory/limits: opposites of limit pullback cones 
-[PR #14452](https://github.com/leanprover-community/mathlib/pull/14452) category_theory/limits: bilimit from kernel 
-[PR #14948](https://github.com/leanprover-community/mathlib/pull/14948) category_theory/limits/construction: Construct finite limits from terminal objects and pullbacks 
-[PR #15269](https://github.com/leanprover-community/mathlib/pull/15269) category_theory/limits/shapes/comm_sq: opposites of is_pullback and is_pushout 
-[PR #14445](https://github.com/leanprover-community/mathlib/pull/14445) category_theory/preadditive: constructing a semiadditive structure from binary biproducts 
-[PR #15096](https://github.com/leanprover-community/mathlib/pull/15096) category_theory/preadditive: left exactness of certain hom functors 
-[PR #14832](https://github.com/leanprover-community/mathlib/pull/14832) category_theory/preadditive: projective iff coyoneda.obj preserves epimorphisms 
-[PR #15100](https://github.com/leanprover-community/mathlib/pull/15100) category_theory/preadditive/*: algebra over endofunctor preadditive and forget additive functor 
-[PR #15455](https://github.com/leanprover-community/mathlib/pull/15455) category_theory/shapes/pullbacks: Pullbacks isomorphic to the opposite of pushouts 
-[PR #14831](https://github.com/leanprover-community/mathlib/pull/14831) category_theory/yoneda: coyoneda.obj_op_op 
-[PR #15327](https://github.com/leanprover-community/mathlib/pull/15327) combinatorics/additive/behrend: Behrend's lower bound on Roth numbers 
-[PR #14070](https://github.com/leanprover-community/mathlib/pull/14070) combinatorics/additive/behrend: Behrend's construction 
-[PR #14697](https://github.com/leanprover-community/mathlib/pull/14697) combinatorics/additive/ruzsa_covering: The Ruzsa covering lemma 
-[PR #14497](https://github.com/leanprover-community/mathlib/pull/14497) combinatorics/set_family/harris_kleitman: The Harris-Kleitman inequality 
-[PR #14475](https://github.com/leanprover-community/mathlib/pull/14475) combinatorics/set_family/intersecting: Intersecting families 
-[PR #14543](https://github.com/leanprover-community/mathlib/pull/14543) combinatorics/set_family/kleitman: Kleitman's bound 
-[PR #15150](https://github.com/leanprover-community/mathlib/pull/15150) combinatorics/simple_graph/basic: `dart.to_prod` is injective 
-[PR #15156](https://github.com/leanprover-community/mathlib/pull/15156) combinatorics/simple_graph/connectivity: operations and lemmas about path type 
-[PR #15153](https://github.com/leanprover-community/mathlib/pull/15153) combinatorics/simple_graph/connectivity: simp confluence 
-[PR #15353](https://github.com/leanprover-community/mathlib/pull/15353) combinatorics/simple_graph/density: Bound on the difference between edge densities 
-[PR #14978](https://github.com/leanprover-community/mathlib/pull/14978) combinatorics/simple_graph/hasse: The Hasse diagram of `α × β` 
-[PR #14867](https://github.com/leanprover-community/mathlib/pull/14867) combinatorics/simple_graph/prod: Box product 
-[PR #13222](https://github.com/leanprover-community/mathlib/pull/13222) combinatorics/simple_graph/regularity/equitabilise: Equitabilising a partition 
-[PR #14403](https://github.com/leanprover-community/mathlib/pull/14403) combinatorics/simple_graph/subgraph: delete vertices in a subgraph 
-[PR #14877](https://github.com/leanprover-community/mathlib/pull/14877) combinatorics/simple_graph/subgraph: add `subgraph.comap` and subgraph of subgraph coercion 
-[PR #15158](https://github.com/leanprover-community/mathlib/pull/15158) combinatorics/simple_graph/trails: Euler's condition for trails  
-[PR #14034](https://github.com/leanprover-community/mathlib/pull/14034) combinatorics/simple_graph/{basic,subgraph,clique,coloring}: add induced graphs, characterization of cliques, and bounds for colorings 
-[PR #15505](https://github.com/leanprover-community/mathlib/pull/15505) computability/ackermann: the Ackermann function isn't primitive recursive 
-[PR #15280](https://github.com/leanprover-community/mathlib/pull/15280) data/countable: add `countable` typeclass 
-[PR #15337](https://github.com/leanprover-community/mathlib/pull/15337) data/fin/basic: add a reflected instance 
-[PR #15048](https://github.com/leanprover-community/mathlib/pull/15048) data/fin/tuple/basic: add lemmas for rewriting exists and forall over `n+1`-tuples 
-[PR #15607](https://github.com/leanprover-community/mathlib/pull/15607) data/finset/basic: There is exactly one set in empty types 
-[PR #15385](https://github.com/leanprover-community/mathlib/pull/15385) data/finset/basic: lemmas about `filter`, `cons`, and `disj_union` 
-[PR #15170](https://github.com/leanprover-community/mathlib/pull/15170) data/finset/basic: Add `decidable_nonempty` for finsets. 
-[PR #15011](https://github.com/leanprover-community/mathlib/pull/15011) data/finset/basic: Coercion of a product of finsets 
-[PR #15257](https://github.com/leanprover-community/mathlib/pull/15257) data/finset/fold: add lemma `fold_max_add` 
-[PR #15212](https://github.com/leanprover-community/mathlib/pull/15212) data/finset/lattice: add three*2 lemmas about `finset.max/min` 
-[PR #15435](https://github.com/leanprover-community/mathlib/pull/15435) data/finset/pointwise: Singleton arithmetic 
-[PR #15387](https://github.com/leanprover-community/mathlib/pull/15387) data/finset/powerset: More `powerset` lemmas 
-[PR #15197](https://github.com/leanprover-community/mathlib/pull/15197) data/finsupp/basic: graph of a finitely supported function 
-[PR #15155](https://github.com/leanprover-community/mathlib/pull/15155) data/finsupp/big_operators: sum of finsupp and their support 
-[PR #15080](https://github.com/leanprover-community/mathlib/pull/15080) data/fintype/basic: add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. 
-[PR #15207](https://github.com/leanprover-community/mathlib/pull/15207) data/json: helper functions for json serialization 
-[PR #15138](https://github.com/leanprover-community/mathlib/pull/15138) data/list: accessing list with fallback 
-[PR #15472](https://github.com/leanprover-community/mathlib/pull/15472) data/list/basic: when drop_while and take_while hold 
-[PR #15482](https://github.com/leanprover-community/mathlib/pull/15482) data/list/basic: last_reverse 
-[PR #15139](https://github.com/leanprover-community/mathlib/pull/15139) data/list/basic: nth_le_enum 
-[PR #14777](https://github.com/leanprover-community/mathlib/pull/14777) data/list/basic: add filter_map_join 
-[PR #15473](https://github.com/leanprover-community/mathlib/pull/15473) data/list/infix: drop_while and take_while suf/prefix 
-[PR #15433](https://github.com/leanprover-community/mathlib/pull/15433) data/list/of_fn: lemmas to turn quantifiers over lists to quantifiers over tuples 
-[PR #15386](https://github.com/leanprover-community/mathlib/pull/15386) data/matrix/basic: Add `alg_equiv` and `linear_equiv` instances for transpose. 
-[PR #14991](https://github.com/leanprover-community/mathlib/pull/14991) data/matrix/notation: add `!![1, 2; 3, 4]` notation 
-[PR #15094](https://github.com/leanprover-community/mathlib/pull/15094) data/multiset/fintype: coercion from multiset to type 
-[PR #15457](https://github.com/leanprover-community/mathlib/pull/15457) data/nat/basic: add recursion principle `even_odd_rec` as a wrapper around `binary_rec` 
-[PR #15061](https://github.com/leanprover-community/mathlib/pull/15061) data/nat/basic: add `strong_sub_recursion` and `pincer_recursion` 
-[PR #15099](https://github.com/leanprover-community/mathlib/pull/15099) data/nat/basic: split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas 
-[PR #15031](https://github.com/leanprover-community/mathlib/pull/15031) data/nat/basic: add `mul_div_mul_comm_of_dvd_dvd` 
-[PR #15409](https://github.com/leanprover-community/mathlib/pull/15409) data/nat/bitwise: tweak `lxor` lemmas 
-[PR #15072](https://github.com/leanprover-community/mathlib/pull/15072) data/nat/choose/basic: Definition of `multichoose` and basic lemmas 
-[PR #15029](https://github.com/leanprover-community/mathlib/pull/15029) data/nat/enat: simple lemmas on `enat` 
-[PR #15767](https://github.com/leanprover-community/mathlib/pull/15767) data/nat/factorization/basic: add lemma `prime.factorization_self` 
-[PR #15277](https://github.com/leanprover-community/mathlib/pull/15277) data/nat/factorization/basic: golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` 
-[PR #15014](https://github.com/leanprover-community/mathlib/pull/15014) data/nat/factorization/basic: add lemma `factorization_eq_card_pow_dvd` 
-[PR #15539](https://github.com/leanprover-community/mathlib/pull/15539) data/nat/pairing: basic bounds on `mkpair` 
-[PR #15268](https://github.com/leanprover-community/mathlib/pull/15268) data/nat/parity: `nat.bit1_div_bit0` 
-[PR #15645](https://github.com/leanprover-community/mathlib/pull/15645) data/nat/totient: lemmas `totient_mul_of_prime_of_{not_}dvd` 
-[PR #15313](https://github.com/leanprover-community/mathlib/pull/15313) data/pfun: tooling to help reasoning about pfun domains 
-[PR #15588](https://github.com/leanprover-community/mathlib/pull/15588) data/pi/algebra: sum_elim lemmas 
-[PR #15508](https://github.com/leanprover-community/mathlib/pull/15508) data/pnat/basic: add lemmas, move `equiv.pnat_equiv_nat` 
-[PR #15183](https://github.com/leanprover-community/mathlib/pull/15183) data/pnat/basic: `succ` as an order isomorphism between `ℕ` and `ℕ+` 
-[PR #15199](https://github.com/leanprover-community/mathlib/pull/15199) data/polynomial/degree/definitions: redefine `polynomial.degree` as `p.support.max` 
-[PR #15522](https://github.com/leanprover-community/mathlib/pull/15522) data/polynomial/degree/lemmas: three lemmas on nat_degrees, bits and neg 
-[PR #14741](https://github.com/leanprover-community/mathlib/pull/14741) data/polynomial/erase_lead: Characterization of polynomials of fixed support 
-[PR #15225](https://github.com/leanprover-community/mathlib/pull/15225) data/polynomial/laurent: define `degree` and some API 
-[PR #15318](https://github.com/leanprover-community/mathlib/pull/15318) data/polynomial/unit_trinomial: Irreducibility of X^n-X-1 
-[PR #14914](https://github.com/leanprover-community/mathlib/pull/14914) data/polynomial/unit_trinomial: An irreducibility criterion for unit trinomials 
-[PR #15148](https://github.com/leanprover-community/mathlib/pull/15148) data/quot: `is_equiv` instance for quotient equivalence 
-[PR #15101](https://github.com/leanprover-community/mathlib/pull/15101) data/rat/defs: add denominator as pnat 
-[PR #15575](https://github.com/leanprover-community/mathlib/pull/15575) data/real/basic: add a repr showing an underlying cauchy sequence 
-[PR #15483](https://github.com/leanprover-community/mathlib/pull/15483) data/real/{e,}nnreal: images and preimages of `ord_connected` sets 
-[PR #14970](https://github.com/leanprover-community/mathlib/pull/14970) data/set/basic,order/filter/basic: add semiconj lemmas about images and maps 
-[PR #15671](https://github.com/leanprover-community/mathlib/pull/15671) data/set/countable: add `iff` versions of some lemmas 
-[PR #15415](https://github.com/leanprover-community/mathlib/pull/15415) data/set/countable: protect lemmas 
-[PR #15444](https://github.com/leanprover-community/mathlib/pull/15444) data/set/finite: set.finite.induction_on' 
-[PR #15177](https://github.com/leanprover-community/mathlib/pull/15177) data/set/finite: add `multiset.finite_to_set` 
-[PR #15605](https://github.com/leanprover-community/mathlib/pull/15605) data/set/function: add lemmas about `set.restrict` 
-[PR #15608](https://github.com/leanprover-community/mathlib/pull/15608) data/set/intervals: add lemmas 
-[PR #14928](https://github.com/leanprover-community/mathlib/pull/14928) data/set/pointwise: `list` and `multiset` versions of n-ary lemmas 
-[PR #15604](https://github.com/leanprover-community/mathlib/pull/15604) data/set/prod: add theorems about `λ x, (x, x)` 
-[PR #15652](https://github.com/leanprover-community/mathlib/pull/15652) data/sign: `left.sign_neg`, `right.sign_neg` 
-[PR #15358](https://github.com/leanprover-community/mathlib/pull/15358) data/sum/basic: `sum.lift_rel` is a subrelation of `sum.lex` 
-[PR #15370](https://github.com/leanprover-community/mathlib/pull/15370) data/sum/order: `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` 
-[PR #15192](https://github.com/leanprover-community/mathlib/pull/15192) data/sym/basic: combinatorial equivalence for `sym (option α) n.succ` 
-[PR #11162](https://github.com/leanprover-community/mathlib/pull/11162) data/sym/card: Prove stars and bars 
-[PR #15383](https://github.com/leanprover-community/mathlib/pull/15383) data/vector/basic: make the recursor work with `induction _ using` syntax 
-[PR #15154](https://github.com/leanprover-community/mathlib/pull/15154) data/vector/mem: Lemmas about membership in a vector 
-[PR #15493](https://github.com/leanprover-community/mathlib/pull/15493) data/{finset,set}/basic: `insert a s = s ↔ a ∈ s` 
-[PR #15478](https://github.com/leanprover-community/mathlib/pull/15478) data/{pi, prod}: add missing `has_pow` instances for `pi` type 
-[PR #15724](https://github.com/leanprover-community/mathlib/pull/15724) field_theory/adjoin: A compositum of algebraic extensions is algebraic 
-[PR #15426](https://github.com/leanprover-community/mathlib/pull/15426) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version 
-[PR #15518](https://github.com/leanprover-community/mathlib/pull/15518) field_theory/adjoin: `intermediate_field.exists_finset_of_mem_supr` 
-[PR #15438](https://github.com/leanprover-community/mathlib/pull/15438) field_theory/adjoin: Compact elements of `intermediate_field` 
-[PR #15420](https://github.com/leanprover-community/mathlib/pull/15420) field_theory/adjoin: `F⟮α⟯ ≤ K ↔ α ∈ K` 
-[PR #15339](https://github.com/leanprover-community/mathlib/pull/15339) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional 
-[PR #15659](https://github.com/leanprover-community/mathlib/pull/15659) field_theory/intermediate_field: Produce an intermediate field from a subalgebra satisfying `is_field`. 
-[PR #15188](https://github.com/leanprover-community/mathlib/pull/15188) field_theory/intermediate_field: `dsimp` lemma 
-[PR #15303](https://github.com/leanprover-community/mathlib/pull/15303) field_theory/tower: if `L / K / F` is finite, so is `K / F` 
-[PR #15021](https://github.com/leanprover-community/mathlib/pull/15021) geometry/euclidean/basic: `continuous_at_angle` 
-[PR #15463](https://github.com/leanprover-community/mathlib/pull/15463) geometry/euclidean/oriented_angle: `continuous_at_oangle` 
-[PR #15560](https://github.com/leanprover-community/mathlib/pull/15560) geometry/manifold: generalize some lemmas from `smooth` to `cont_mdiff` 
-[PR #15116](https://github.com/leanprover-community/mathlib/pull/15116) geometry/manifold/local_invariant_properties: simplify definitions and proofs 
-[PR #15437](https://github.com/leanprover-community/mathlib/pull/15437) geometry/manifold/metrizable: metrizability of a manifold 
-[PR #15314](https://github.com/leanprover-community/mathlib/pull/15314) geometry/manifold|topology: add simps and ext attributes 
-[PR #14182](https://github.com/leanprover-community/mathlib/pull/14182) group_theory/complement: transversal for the transfer homomorphism 
-[PR #15402](https://github.com/leanprover-community/mathlib/pull/15402) group_theory/finite_abelian: a finitely generated torsion abelian group is finite 
-[PR #15239](https://github.com/leanprover-community/mathlib/pull/15239) group_theory/group_action/option: Scalar action on an option 
-[PR #15050](https://github.com/leanprover-community/mathlib/pull/15050) group_theory/group_action/sub_mul_action: add the pointwise monoid structure 
-[PR #8632](https://github.com/leanprover-community/mathlib/pull/8632) group_theory/p_group: Groups of order p^2 are commutative 
-[PR #15052](https://github.com/leanprover-community/mathlib/pull/15052) group_theory/submonoid/pointwise: add the pointwise monoid structure on `add_submonoid` 
-[PR #13945](https://github.com/leanprover-community/mathlib/pull/13945) group_theory/subsemigroup/membership: add membership criteria for subsemigroups 
-[PR #14739](https://github.com/leanprover-community/mathlib/pull/14739) information_theory/hamming: add Hamming distance and norm 
-[PR #15603](https://github.com/leanprover-community/mathlib/pull/15603) integration: elementary version of FTC-1 
-[PR #15587](https://github.com/leanprover-community/mathlib/pull/15587) linear_algebra: lemmas on associatedness of determinants of linear maps 
-[PR #15119](https://github.com/leanprover-community/mathlib/pull/15119) linear_algebra: basis on R × R, and relation between matrices and linear maps in this basis  
-[PR #14714](https://github.com/leanprover-community/mathlib/pull/14714) linear_algebra/*: add lemma `linear_independent.finite_of_is_noetherian` 
-[PR #12140](https://github.com/leanprover-community/mathlib/pull/12140) linear_algebra/annihilating_polynomial: add definition of annihilating ideal and show minpoly generates in field case 
-[PR #14883](https://github.com/leanprover-community/mathlib/pull/14883) linear_algebra/basis: shows the lattice of submodules of a module over a division ring is atomistic 
-[PR #14790](https://github.com/leanprover-community/mathlib/pull/14790) linear_algebra/clifford_algebra/even: Universal property and isomorphisms for the even subalgebra 
-[PR #15558](https://github.com/leanprover-community/mathlib/pull/15558) linear_algebra/finite_dimensional: One-dimensional iff principal 
-[PR #15531](https://github.com/leanprover-community/mathlib/pull/15531) linear_algebra/linear_pmap: more lemmas about the graph 
-[PR #14922](https://github.com/leanprover-community/mathlib/pull/14922) linear_algebra/linear_pmap: construct a `linear_pmap` from its graph 
-[PR #14794](https://github.com/leanprover-community/mathlib/pull/14794) linear_algebra/matrix: inner prod of matrix 
-[PR #15459](https://github.com/leanprover-community/mathlib/pull/15459) linear_algebra/matrix/charpoly: Coefficients of the characteristic polynomial falls in the ideal power. 
-[PR #15391](https://github.com/leanprover-community/mathlib/pull/15391) linear_algebra/projective_space/subspace: defines subspaces of a projective space 
-[PR #14542](https://github.com/leanprover-community/mathlib/pull/14542) linear_algebra/projectivization/independence: defines (in)dependence of points in projective space 
-[PR #15628](https://github.com/leanprover-community/mathlib/pull/15628) linear_algebra/tensor_product: add id_apply and comp_apply for ltensor and rtensor 
-[PR #15209](https://github.com/leanprover-community/mathlib/pull/15209) linear_algebra/unitary_group: better constructor 
-[PR #15524](https://github.com/leanprover-community/mathlib/pull/15524) logic/encodable/basic: an encodable type is countable 
-[PR #15611](https://github.com/leanprover-community/mathlib/pull/15611) logic/equiv/local_equiv: add 2 lemmas 
-[PR #15176](https://github.com/leanprover-community/mathlib/pull/15176) logic/equiv/set: define `equiv.set.pi` 
-[PR #15574](https://github.com/leanprover-community/mathlib/pull/15574) logic/nonempty: `pi.nonempty` instance 
-[PR #15307](https://github.com/leanprover-community/mathlib/pull/15307) measure_theory/constructions/borel_space: the set of points for which a measurable sequence of functions converges is measurable 
-[PR #14424](https://github.com/leanprover-community/mathlib/pull/14424) measure_theory/constructions/prod: The layercake integral. 
-[PR #15422](https://github.com/leanprover-community/mathlib/pull/15422) measure_theory/function/conditional_expecation: conditional expectation of a function to a independent sigma-algebra  
-[PR #15274](https://github.com/leanprover-community/mathlib/pull/15274) measure_theory/function/conditional_expectation: pull-out property of the conditional expectation 
-[PR #15024](https://github.com/leanprover-community/mathlib/pull/15024) measure_theory/function/conditional_expectation: monotonicity of the conditional expectation 
-[PR #15378](https://github.com/leanprover-community/mathlib/pull/15378) measure_theory/function/uniform_integrable: conditional expectations form a uniformly integrable class 
-[PR #15120](https://github.com/leanprover-community/mathlib/pull/15120) measure_theory/group/measure: a product of Haar measures is a Haar measure 
-[PR #15423](https://github.com/leanprover-community/mathlib/pull/15423) measure_theory/integral: generalize some integral properties to set_to_fun 
-[PR #13885](https://github.com/leanprover-community/mathlib/pull/13885) measure_theory/integral: Circle integral transform 
-[PR #15344](https://github.com/leanprover-community/mathlib/pull/15344) measure_theory/integral/set_integral: add `set_integral_indicator` 
-[PR #15342](https://github.com/leanprover-community/mathlib/pull/15342) measure_theory/measurable_space_def: add `generate_from_induction` 
-[PR #15528](https://github.com/leanprover-community/mathlib/pull/15528) measure_theory/measure/finite_measure_weak_convergence: Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. 
-[PR #15205](https://github.com/leanprover-community/mathlib/pull/15205) measure_theory/measure/finite_measure_weak_convergence: Add some missing API lemmas. 
-[PR #15343](https://github.com/leanprover-community/mathlib/pull/15343) measure_theory/measure/measure_space: generalize measure.comap 
-[PR #15066](https://github.com/leanprover-community/mathlib/pull/15066) measure_theory/pmf: lawful monad instance for probability mass function monad 
-[PR #8002](https://github.com/leanprover-community/mathlib/pull/8002) number_theory: Bertrand's postulate, slightly different approach 
-[PR #15315](https://github.com/leanprover-community/mathlib/pull/15315) number_theory: degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` 
-[PR #15418](https://github.com/leanprover-community/mathlib/pull/15418) number_theory/legendre_symbol/*: redefine quadratic characters as `mul_char`s 
-[PR #15499](https://github.com/leanprover-community/mathlib/pull/15499) number_theory/legendre_symbol/add_character: add file introducing additive characters 
-[PR #15007](https://github.com/leanprover-community/mathlib/pull/15007) number_theory/slash_actions: Slash actions class for modular forms 
-[PR #14717](https://github.com/leanprover-community/mathlib/pull/14717) number_theory/wilson: add Wilson's Theorem 
-[PR #15149](https://github.com/leanprover-community/mathlib/pull/15149) order/basic: a symmetric relation implies equality when it implies less-equal 
-[PR #15606](https://github.com/leanprover-community/mathlib/pull/15606) order/boolean_algebra: A bounded generalized boolean algebra is a boolean algebra 
-[PR #15278](https://github.com/leanprover-community/mathlib/pull/15278) order/bounded_order: `is_well_order` instances for `with_top` and `with_bot` 
-[PR #15636](https://github.com/leanprover-community/mathlib/pull/15636) order/bounded_order: an order is either an `order_bot` or a `no_bot_order` 
-[PR #15341](https://github.com/leanprover-community/mathlib/pull/15341) order/bounded_order: two lemmas about the interaction between monotonicity and map with_bot/top 
-[PR #15357](https://github.com/leanprover-community/mathlib/pull/15357) order/bounded_order: `subrelation r s ↔ r ≤ s` 
-[PR #14195](https://github.com/leanprover-community/mathlib/pull/14195) order/bounded_order: Codisjointness 
-[PR #15665](https://github.com/leanprover-community/mathlib/pull/15665) order/compare: general cleanup 
-[PR #15340](https://github.com/leanprover-community/mathlib/pull/15340) order/complete_boolean_algebra: A frame is distributive 
-[PR #15237](https://github.com/leanprover-community/mathlib/pull/15237) order/filter: add `map_neg_at_top`, change some assumptions 
-[PR #15632](https://github.com/leanprover-community/mathlib/pull/15632) order/filter/*: `filter.pi` is countably generated 
-[PR #15630](https://github.com/leanprover-community/mathlib/pull/15630) order/filter/bases: lemmas about bases of product filters 
-[PR #15661](https://github.com/leanprover-community/mathlib/pull/15661) order/filter/basic: add `filter.has_basis.bInter_mem` 
-[PR #15128](https://github.com/leanprover-community/mathlib/pull/15128) order/filter/basic: add `map_le_map` and `map_injective` 
-[PR #15187](https://github.com/leanprover-community/mathlib/pull/15187) order/filter/ultrafilter: `pure`, `map`, and `comap` lemmas 
-[PR #15432](https://github.com/leanprover-community/mathlib/pull/15432) order/hom/basic: `order_iso` of `rel_iso (<) (<)` 
-[PR #15182](https://github.com/leanprover-community/mathlib/pull/15182) order/hom/basic: `order_iso` to `rel_iso (<) (<)` 
-[PR #15375](https://github.com/leanprover-community/mathlib/pull/15375) order/initial_seg: Initial/principal segment from empty type 
-[PR #15374](https://github.com/leanprover-community/mathlib/pull/15374) order/initial_seg: remove `nolint` from `initial_seg` 
-[PR #15439](https://github.com/leanprover-community/mathlib/pull/15439) order/lattice: Congruence lemmas for `⊔` and `⊓` 
-[PR #14789](https://github.com/leanprover-community/mathlib/pull/14789) order/lattice, data/set: some helper lemmas 
-[PR #15136](https://github.com/leanprover-community/mathlib/pull/15136) order/lattice, order/lattice_intervals: coe inf/sup lemmas 
-[PR #14733](https://github.com/leanprover-community/mathlib/pull/14733) order/locally_finite: make `fintype.to_locally_finite_order` computable 
-[PR #11602](https://github.com/leanprover-community/mathlib/pull/11602) order/modular_lattice: Semimodular lattices 
-[PR #15073](https://github.com/leanprover-community/mathlib/pull/15073) order/order_iso_nat: generalize `well_founded.monotone_chain_condition` to preorders 
-[PR #15350](https://github.com/leanprover-community/mathlib/pull/15350) order/partition/finpartition: Bound size of a bit of `finpartition.atomise` 
-[PR #15430](https://github.com/leanprover-community/mathlib/pull/15430) order/rel_iso: add lemmas on `rel_iso.cast` 
-[PR #15372](https://github.com/leanprover-community/mathlib/pull/15372) order/rel_iso: relation embedding from empty type 
-[PR #14760](https://github.com/leanprover-community/mathlib/pull/14760) order/rel_iso: two reflexive/irreflexive relations on a unique type are isomorphic 
-[PR #15144](https://github.com/leanprover-community/mathlib/pull/15144) order/rel_iso: add `rel_iso.cast` 
-[PR #15016](https://github.com/leanprover-community/mathlib/pull/15016) order/succ_pred: expand API on `with_bot` and `with_top` 
-[PR #15567](https://github.com/leanprover-community/mathlib/pull/15567) order/succ_pred/basic: `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related 
-[PR #15536](https://github.com/leanprover-community/mathlib/pull/15536) order/succ_pred/basic: `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses 
-[PR #15001](https://github.com/leanprover-community/mathlib/pull/15001) order/succ_pred/limit: Successor and predecessor limits 
-[PR #15581](https://github.com/leanprover-community/mathlib/pull/15581) order/upper_lower: Upper closure of a set 
-[PR #15399](https://github.com/leanprover-community/mathlib/pull/15399) order/well_founded: typeclasses for well-founded `<` and `>` 
-[PR #15266](https://github.com/leanprover-community/mathlib/pull/15266) order/well_founded_set: any relation is well-founded on `Ø` 
-[PR #15678](https://github.com/leanprover-community/mathlib/pull/15678) probability/density: probability of event in uniform distribution 
-[PR #15131](https://github.com/leanprover-community/mathlib/pull/15131) probability/independence: two tuples indexed by disjoint subsets of an independent family of r.v. are independent 
-[PR #14909](https://github.com/leanprover-community/mathlib/pull/14909) probability/martingale: the discrete stochastic integral of a submartingale is a submartingale 
-[PR #14737](https://github.com/leanprover-community/mathlib/pull/14737) probability/martingale: Doob's maximal inequality 
-[PR #14932](https://github.com/leanprover-community/mathlib/pull/14932) probability/martingale: positive part of a submartingale is also a submartingale 
-[PR #15140](https://github.com/leanprover-community/mathlib/pull/15140) probability/moments: mgf/cgf of a sum of independent random variables 
-[PR #15129](https://github.com/leanprover-community/mathlib/pull/15129) probability/moments: Chernoff bound on the upper/lower tail of a real random variable 
-[PR #15392](https://github.com/leanprover-community/mathlib/pull/15392) probability/strong_law: Lp version of the strong law of large numbers 
-[PR #14331](https://github.com/leanprover-community/mathlib/pull/14331) representation_theory/Action: mapping by a monoidal functor 
-[PR #13713](https://github.com/leanprover-community/mathlib/pull/13713) representation_theory/Rep: Rep k G ≌ Module (monoid_algebra k G) 
-[PR #15084](https://github.com/leanprover-community/mathlib/pull/15084) representation_theory/character: formula for the dimension of the invariants in terms of the character 
-[PR #14308](https://github.com/leanprover-community/mathlib/pull/14308) representation_theory/monoid_algebra_basis: add some API for `k[G^n]` 
-[PR #15243](https://github.com/leanprover-community/mathlib/pull/15243) ring_theory: Formally étale/smooth/unramified morphisms are stable under base change. 
-[PR #14348](https://github.com/leanprover-community/mathlib/pull/14348) ring_theory: the Ore localization of a ring 
-[PR #15381](https://github.com/leanprover-community/mathlib/pull/15381) ring_theory: the integral closure `C` of `A` is Noetherian over `A` 
-[PR #14966](https://github.com/leanprover-community/mathlib/pull/14966) ring_theory: Basic framework for classes of ring homomorphisms 
-[PR #15064](https://github.com/leanprover-community/mathlib/pull/15064) ring_theory: Some missing lemmas 
-[PR #15333](https://github.com/leanprover-community/mathlib/pull/15333) ring_theory/I_filtration: I-filtrations of modules. 
-[PR #14981](https://github.com/leanprover-community/mathlib/pull/14981) ring_theory/adjoin_root: add lemmas for GCD domains 
-[PR #15586](https://github.com/leanprover-community/mathlib/pull/15586) ring_theory/algebraic: `is_algebraic_algebra_map_iff` 
-[PR #15424](https://github.com/leanprover-community/mathlib/pull/15424) ring_theory/bezout: Bezout domains are integrally closed 
-[PR #15091](https://github.com/leanprover-community/mathlib/pull/15091) ring_theory/bezout: Define Bézout rings. 
-[PR #11053](https://github.com/leanprover-community/mathlib/pull/11053) ring_theory/dedekind_domain: If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape 
-[PR #15244](https://github.com/leanprover-community/mathlib/pull/15244) ring_theory/derivation: Derivations into square-zero ideals corresponds to liftings.  
-[PR #15242](https://github.com/leanprover-community/mathlib/pull/15242) ring_theory/etale: Formally étale morphisms. 
-[PR #15264](https://github.com/leanprover-community/mathlib/pull/15264) ring_theory/graded_algebra/basic: add lemma `proj_homogeneous_mul` 
-[PR #15460](https://github.com/leanprover-community/mathlib/pull/15460) ring_theory/ideal/operations: A variant of `finsupp.total` for ideals. 
-[PR #12812](https://github.com/leanprover-community/mathlib/pull/12812) ring_theory/integrally_closed: if x is in Frac R such that x^n is in R then x is in R 
-[PR #15404](https://github.com/leanprover-community/mathlib/pull/15404) ring_theory/localization/basic: section of localisation of non-zero is non-zero 
-[PR #15261](https://github.com/leanprover-community/mathlib/pull/15261) ring_theory/localization/basic: add `mk_sum` 
-[PR #15561](https://github.com/leanprover-community/mathlib/pull/15561) ring_theory/noetherian: Finitely generated idempotent ideal is principal. 
-[PR #15397](https://github.com/leanprover-community/mathlib/pull/15397) ring_theory/power_series/basic: Add `rescale_X` 
-[PR #15287](https://github.com/leanprover-community/mathlib/pull/15287) ring_theory/power_series/well_known: Coefficients of sin and cos 
-[PR #15089](https://github.com/leanprover-community/mathlib/pull/15089) ring_theory/rees_algebra: Define the Rees algebra of an ideal. 
-[PR #15427](https://github.com/leanprover-community/mathlib/pull/15427) ring_theory/ring_hom/finite: Finite ring morphisms are stable under base change 
-[PR #15379](https://github.com/leanprover-community/mathlib/pull/15379) ring_theory/ring_hom/finite: Finite type is a local property 
-[PR #15512](https://github.com/leanprover-community/mathlib/pull/15512) ring_theory/tensor_product: A predicate for being the tensor product. 
-[PR #15241](https://github.com/leanprover-community/mathlib/pull/15241) ring_theory/tensor_product: `A`-algebra structure on `A' ⊗[R] B`. 
-[PR #15093](https://github.com/leanprover-community/mathlib/pull/15093) ring_theory/valuation: Properties of valuation rings. 
-[PR #14896](https://github.com/leanprover-community/mathlib/pull/14896) set/intervals/monotone: add some monotonicity lemmas 
-[PR #14989](https://github.com/leanprover-community/mathlib/pull/14989) set_theory/cardinal/ordinal: basic properties on Beth numbers 
-[PR #15198](https://github.com/leanprover-community/mathlib/pull/15198) set_theory/cardinal/ordinal: cardinality of `α →₀ β` 
-[PR #15367](https://github.com/leanprover-community/mathlib/pull/15367) set_theory/game/nim: make the file `noncomputable theory` 
-[PR #14780](https://github.com/leanprover-community/mathlib/pull/14780) set_theory/game/ordinal: lemmas on `0.to_pgame` and `1.to_pgame` 
-[PR #15255](https://github.com/leanprover-community/mathlib/pull/15255) set_theory/game/pgame: strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` 
-[PR #15256](https://github.com/leanprover-community/mathlib/pull/15256) set_theory/game/pgame: `is_option (-x) (-y) ↔ is_option x y` 
-[PR #15254](https://github.com/leanprover-community/mathlib/pull/15254) set_theory/game/pgame: add `equiv.comm` 
-[PR #15533](https://github.com/leanprover-community/mathlib/pull/15533) set_theory/ordinal/arithmetic: `pred 0 = 0` 
-[PR #15447](https://github.com/leanprover-community/mathlib/pull/15447) set_theory/ordinal/arithmetic: more log lemmas 
-[PR #15193](https://github.com/leanprover-community/mathlib/pull/15193) set_theory/ordinal/arithmetic: tweak `type_add` and `type_mul` 
-[PR #15174](https://github.com/leanprover-community/mathlib/pull/15174) set_theory/ordinal/arithmetic: tweak theorems about `0` and `1` 
-[PR #15348](https://github.com/leanprover-community/mathlib/pull/15348) set_theory/ordinal/basic: dot notation lemmas + golf 
-[PR #15152](https://github.com/leanprover-community/mathlib/pull/15152) set_theory/ordinal/basic: add `gc_ord_card` and `gci_ord_card` 
-[PR #15194](https://github.com/leanprover-community/mathlib/pull/15194) set_theory/ordinal/basic: mark `type_fintype` as `simp` 
-[PR #15178](https://github.com/leanprover-community/mathlib/pull/15178) set_theory/ordinal/basic: order type of naturals is `ω` 
-[PR #15146](https://github.com/leanprover-community/mathlib/pull/15146) set_theory/ordinal/basic: basic lemmas on `ordinal.lift`  
-[PR #15320](https://github.com/leanprover-community/mathlib/pull/15320) set_theory/zfc: ZFC sets are small types 
-[PR #15223](https://github.com/leanprover-community/mathlib/pull/15223) set_theory/zfc: `Ø ⊆ x` 
-[PR #15213](https://github.com/leanprover-community/mathlib/pull/15213) set_theory/zfc: `∈` is well-founded 
-[PR #15324](https://github.com/leanprover-community/mathlib/pull/15324) set_theory/zfc: more `quotient` lemmas 
-[PR #15214](https://github.com/leanprover-community/mathlib/pull/15214) set_theory/zfc: simp lemmas for `arity` and `const` 
-[PR #15211](https://github.com/leanprover-community/mathlib/pull/15211) set_theory/zfc: basic lemmas on `pSet.equiv` 
-[PR #15545](https://github.com/leanprover-community/mathlib/pull/15545) set_theory/zfc/basic: `inj` lemmas 
-[PR #15544](https://github.com/leanprover-community/mathlib/pull/15544) set_theory/zfc/basic: `∈` is well-founded on classes 
-[PR #15573](https://github.com/leanprover-community/mathlib/pull/15573) set_theory/zfc/basic: `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` 
-[PR #15551](https://github.com/leanprover-community/mathlib/pull/15551) set_theory/zfc/basic: `⊆` is reflexive, transitive, antisymmetric 
-[PR #15549](https://github.com/leanprover-community/mathlib/pull/15549) set_theory/zfc/basic: add `refl`, `symm`, `trans` attributes to `equiv` lemmas 
-[PR #15548](https://github.com/leanprover-community/mathlib/pull/15548) set_theory/zfc/ordinal: more lemmas on transitive sets 
-[PR #15288](https://github.com/leanprover-community/mathlib/pull/15288) set_theory/zfc/ordinal: transitive sets 
-[PR #15498](https://github.com/leanprover-community/mathlib/pull/15498) tactic/attribute: add `expand_exists` 
-[PR #14762](https://github.com/leanprover-community/mathlib/pull/14762) tactic/compute_degree + test/compute_degree: introduce a tactic for proving `f.(nat_)degree ≤ d` 
-[PR #14532](https://github.com/leanprover-community/mathlib/pull/14532) tactic/congrm: add "function underscores" to `congrm` 
-[PR #15502](https://github.com/leanprover-community/mathlib/pull/15502) tactic/ext: don't remove attr 
-[PR #15319](https://github.com/leanprover-community/mathlib/pull/15319) tactic/linear_combination: allow linear_combination to leave goal open 
-[PR #15284](https://github.com/leanprover-community/mathlib/pull/15284) tactic/linear_combination: add parser for `h / a` 
-[PR #15202](https://github.com/leanprover-community/mathlib/pull/15202) tactic/lint: add a linter for `[fintype _]` assumptions 
-[PR #14878](https://github.com/leanprover-community/mathlib/pull/14878) tactic/polyrith: a tactic using Sage to solve polynomial equalities with hypotheses 
-[PR #15618](https://github.com/leanprover-community/mathlib/pull/15618) tactic/positivity: a tactic for proving positivity/nonnegativity 
-[PR #15728](https://github.com/leanprover-community/mathlib/pull/15728) test/polyrith: better formatting for generated tests 
-[PR #15641](https://github.com/leanprover-community/mathlib/pull/15641) tooplogy/metric_space/hausdorff_distance: add lemmas about `thickening` 
-[PR #15102](https://github.com/leanprover-community/mathlib/pull/15102) topology: basic simplification lemmas for `continuous_map`s 
-[PR #14806](https://github.com/leanprover-community/mathlib/pull/14806) topology/algebra/filter_basis: add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group 
-[PR #15157](https://github.com/leanprover-community/mathlib/pull/15157) topology/algebra/infinite_sum: Double sum is equal to a single value 
-[PR #15610](https://github.com/leanprover-community/mathlib/pull/15610) topology/algebra/module/finite_dimension: add 2 simp lemmas 
-[PR #15022](https://github.com/leanprover-community/mathlib/pull/15022) topology/algebra/order: ⁻¹ continuous for linear ordered fields 
-[PR #14889](https://github.com/leanprover-community/mathlib/pull/14889) topology/algebra/uniform_group: `uniform_group` is preserved by Inf and comap 
-[PR #15653](https://github.com/leanprover-community/mathlib/pull/15653) topology/basic: add lemmas about `filter.lift' _ closure` 
-[PR #15580](https://github.com/leanprover-community/mathlib/pull/15580) topology/basic: a condition implying that a sequence of functions locally stabilizes 
-[PR #15485](https://github.com/leanprover-community/mathlib/pull/15485) topology/basic: add 2 lemmas about `locally_finite` families 
-[PR #14036](https://github.com/leanprover-community/mathlib/pull/14036) topology/continuous_function: Any T0 space embeds in a product of copies of the Sierpinski space 
-[PR #14724](https://github.com/leanprover-community/mathlib/pull/14724) topology/homotopy: define nth homotopy group πₙ (without the group instance) 
-[PR #15593](https://github.com/leanprover-community/mathlib/pull/15593) topology/instances/ennreal: add `continuous(_on).ennreal_mul` 
-[PR #15446](https://github.com/leanprover-community/mathlib/pull/15446) topology/instances/nnreal: add `can_lift C(X, ℝ) C(X, ℝ≥0)` 
-[PR #15311](https://github.com/leanprover-community/mathlib/pull/15311) topology/local_homeomorph: "injectivity" local_homeomorph.prod 
-[PR #15612](https://github.com/leanprover-community/mathlib/pull/15612) topology/maps: add 2 lemmas, `open function` 
-[PR #15165](https://github.com/leanprover-community/mathlib/pull/15165) topology/maps: more `iff` lemmas 
-[PR #14926](https://github.com/leanprover-community/mathlib/pull/14926) topology/metric_space/hausdorff_distance: Thickening a compact inside an open 
-[PR #15591](https://github.com/leanprover-community/mathlib/pull/15591) topology/metric_space/isometry: use namespace, add lemmas 
-[PR #15634](https://github.com/leanprover-community/mathlib/pull/15634) topology/metric_space/lipschitz: add several lemmas 
-[PR #14965](https://github.com/leanprover-community/mathlib/pull/14965) topology/noetherian_space: Noetherian spaces 
-[PR #15617](https://github.com/leanprover-community/mathlib/pull/15617) topology/order: upgrade some lemmas to `iff`s 
-[PR #15490](https://github.com/leanprover-community/mathlib/pull/15490) topology/partition_of_unity: local to global 
-[PR #15635](https://github.com/leanprover-community/mathlib/pull/15635) topology/separation: add `disjoint_nhds_nhds` 
-[PR #15043](https://github.com/leanprover-community/mathlib/pull/15043) topology/separation: `separation_quotient α` is a T₀ space 
-[PR #15338](https://github.com/leanprover-community/mathlib/pull/15338) topology/sets/closeds: The coframe of closed sets 
-[PR #15118](https://github.com/leanprover-community/mathlib/pull/15118) topology/sets/compacts: prod constructions 
-[PR #15707](https://github.com/leanprover-community/mathlib/pull/15707) topology/subset_properties: `locally_compact_space` instance for `Π` types 
-[PR #15484](https://github.com/leanprover-community/mathlib/pull/15484) topology/support: add lemmas, fix a name 
-[PR #15346](https://github.com/leanprover-community/mathlib/pull/15346) topology/support: tsupport of product is a subset of tsupport 
-[PR #14892](https://github.com/leanprover-community/mathlib/pull/14892) topology/uniform_space/basic: uniform continuity from/to an infimum of uniform spaces 
+* [PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) add lemmas about sigma types 
+* [PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) /partition_of_unity: more lemmas based on the partition of unity 
+* [PR #15744](https://github.com/leanprover-community/mathlib/pull/15744) algebra/algebra/subalgebra/basic: Swap arguments of `map` and `comap` 
+* [PR #15556](https://github.com/leanprover-community/mathlib/pull/15556) algebra/big_operators: add lemmas about sum of disjoint multiset 
+* [PR #15095](https://github.com/leanprover-community/mathlib/pull/15095) algebra/category: forgetful functors from modules reflect limits 
+* [PR #15019](https://github.com/leanprover-community/mathlib/pull/15019) algebra/category/BoolRing: The equivalence between Boolean rings and Boolean algebras 
+* [PR #15330](https://github.com/leanprover-community/mathlib/pull/15330) algebra/category/Group: The forgetful-units adjunction between `Group` and `Mon`. 
+* [PR #14328](https://github.com/leanprover-community/mathlib/pull/14328) algebra/category/Module: upgrade `free : Type ⥤ Module R` to a monoidal functor 
+* [PR #14720](https://github.com/leanprover-community/mathlib/pull/14720) algebra/category_theory/Group/epi_mono: about monomorphism and epimorphism in category of group 
+* [PR #15654](https://github.com/leanprover-community/mathlib/pull/15654) algebra/direct_sum/decomposition: add an induction principle for `direct_sum.decomposition` class 
+* [PR #15109](https://github.com/leanprover-community/mathlib/pull/15109) algebra/gcd_monoid: GCD domains are integrally closed. 
+* [PR #15403](https://github.com/leanprover-community/mathlib/pull/15403) algebra/group/with_one: units of a group with zero is isomorphic to the group 
+* [PR #14945](https://github.com/leanprover-community/mathlib/pull/14945) algebra/homology: homotopy equivalences are quasi-isomorphisms 
+* [PR #11073](https://github.com/leanprover-community/mathlib/pull/11073) algebra/jordan: Introduce Jordan rings 
+* [PR #14179](https://github.com/leanprover-community/mathlib/pull/14179) algebra/lie/cartan_subalgebra: characterise Cartan subalgebras as limiting values of upper central series 
+* [PR #15675](https://github.com/leanprover-community/mathlib/pull/15675) algebra/lie/of_associative: add `commute.lie_eq` 
+* [PR #15733](https://github.com/leanprover-community/mathlib/pull/15733) algebra/module: sub_mem_sup for modules over rings 
+* [PR #12895](https://github.com/leanprover-community/mathlib/pull/12895) algebra/module: add injective module and Baer's criterion 
+* [PR #15103](https://github.com/leanprover-community/mathlib/pull/15103) algebra/module/linear_map: use morphisms class for lemmas about linear [pre]images of `c • S` 
+* [PR #14470](https://github.com/leanprover-community/mathlib/pull/14470) algebra/module/localized_module: construction of module localisation 
+* [PR #15092](https://github.com/leanprover-community/mathlib/pull/15092) algebra/module/torsion: `R/I`-module structure on `M/IM`. 
+* [PR #3292](https://github.com/leanprover-community/mathlib/pull/3292) algebra/order/complete_field: `conditionally_complete_linear_ordered_field`, aka the reals 
+* [PR #15300](https://github.com/leanprover-community/mathlib/pull/15300) algebra/order/monoid: add lemmas `map_add` for `with_bot/top` 
+* [PR #15458](https://github.com/leanprover-community/mathlib/pull/15458) algebra/order/monoid: add `one_lt_mul_iff`/`add_pos_iff` 
+* [PR #15219](https://github.com/leanprover-community/mathlib/pull/15219) algebra/order/monoid: Add zero_le_three and zero_le_four 
+* [PR #15267](https://github.com/leanprover-community/mathlib/pull/15267) algebra/order/monoid_lemmas: add `antitone`, `monotone_on`, and `antitone_on` lemmas 
+* [PR #14761](https://github.com/leanprover-community/mathlib/pull/14761) algebra/order/monoid_lemmas_zero_lt: add some lemmas about typeclasses 
+* [PR #14770](https://github.com/leanprover-community/mathlib/pull/14770) algebra/order/monoid_lemmas_zero_lt: add missing lemmas 
+* [PR #15186](https://github.com/leanprover-community/mathlib/pull/15186) algebra/parity: more general odd.pos 
+* [PR #15660](https://github.com/leanprover-community/mathlib/pull/15660) algebra/periodic: `fract_periodic` 
+* [PR #13958](https://github.com/leanprover-community/mathlib/pull/13958) algebra/ring/{pi, prod, opposite}: add basic defs for non_unital_ring_hom 
+* [PR #15291](https://github.com/leanprover-community/mathlib/pull/15291) algebraic_geometry: comap of surjective homomorphism is closed embedding 
+* [PR #11649](https://github.com/leanprover-community/mathlib/pull/11649) algebraic_geometry: Intersection of affine open can be covered by common basic opens 
+* [PR #14972](https://github.com/leanprover-community/mathlib/pull/14972) algebraic_geometry: Restriction of morphisms onto open sets of the target 
+* [PR #15487](https://github.com/leanprover-community/mathlib/pull/15487) algebraic_geometry/AffineScheme: Affine communication lemma 
+* [PR #15365](https://github.com/leanprover-community/mathlib/pull/15365) algebraic_geometry/EllipticCurve: simplify definition of discriminant 
+* [PR #15436](https://github.com/leanprover-community/mathlib/pull/15436) algebraic_geometry/morphisms: Quasi-compact morphisms of schemes 
+* [PR #14944](https://github.com/leanprover-community/mathlib/pull/14944) algebraic_geometry/morphisms: Basic framework for classes of morphisms between schemes 
+* [PR #13397](https://github.com/leanprover-community/mathlib/pull/13397) algebraic_geometry/projective_spectrum: forward direction of homeomorphism between top_space of Proj and top_space of Spec 
+* [PR #14588](https://github.com/leanprover-community/mathlib/pull/14588) algebraic_topology: alternating_coface_map_complex 
+* [PR #15616](https://github.com/leanprover-community/mathlib/pull/15616) algebraic_topology/dold_kan: construction of idempotent endomorphisms 
+* [PR #14044](https://github.com/leanprover-community/mathlib/pull/14044) algebraic_topology/dold_kan: technical lemmas about face maps 
+* [PR #12788](https://github.com/leanprover-community/mathlib/pull/12788) algebraic_topology/fundamental_groupoid: Define simply connected spaces 
+* [PR #15568](https://github.com/leanprover-community/mathlib/pull/15568) analysis/asymptotics: add `is_o*.of_pow` 
+* [PR #15010](https://github.com/leanprover-community/mathlib/pull/15010) analysis/asymptotics/asymptotics: generalize, golf 
+* [PR #15416](https://github.com/leanprover-community/mathlib/pull/15416) analysis/calculus: generalize `differentiable*.pow`, add `differentiable*.zpow` 
+* [PR #15595](https://github.com/leanprover-community/mathlib/pull/15595) analysis/calculus/cont_diff: generalize `mul` lemmas to a normed algebra 
+* [PR #15309](https://github.com/leanprover-community/mathlib/pull/15309) analysis/calculus/cont_diff: extra lemmas about cont_diff_within_at 
+* [PR #15133](https://github.com/leanprover-community/mathlib/pull/15133) analysis/calculus/mean_value: remove assumption in strict_mono_on.strict_convex_on_of_deriv 
+* [PR #15122](https://github.com/leanprover-community/mathlib/pull/15122) analysis/complex: equiv_real_prod_symm_apply 
+* [PR #15364](https://github.com/leanprover-community/mathlib/pull/15364) analysis/complex/abs_max: add a version of the maximum modulus principle 
+* [PR #15639](https://github.com/leanprover-community/mathlib/pull/15639) analysis/convex/cone: add inner_dual_cone_eq_Inter_inner_dual_cone_singleton 
+* [PR #14821](https://github.com/leanprover-community/mathlib/pull/14821) analysis/convex/function: Variants of `convex_on.le_right_of_left_le` 
+* [PR #15363](https://github.com/leanprover-community/mathlib/pull/15363) analysis/inner_product/calculus: [higher] differentiability to/from `euclidean_space` 
+* [PR #15481](https://github.com/leanprover-community/mathlib/pull/15481) analysis/inner_product/pi_L2: a finite orthonormal family is a basis of its span 
+* [PR #15540](https://github.com/leanprover-community/mathlib/pull/15540) analysis/inner_product_space: in finite dimension, hilbert basis = orthonormal basis 
+* [PR #15055](https://github.com/leanprover-community/mathlib/pull/15055) analysis/inner_product_space: the Hellinger-Toeplitz theorem 
+* [PR #15020](https://github.com/leanprover-community/mathlib/pull/15020) analysis/inner_product_space: add simple lemmas for the orthogonal complement 
+* [PR #15514](https://github.com/leanprover-community/mathlib/pull/15514) analysis/inner_product_space/[pi_L2, l2_space]: compute inner product in a given [orthonormal, hilbert] basis 
+* [PR #15577](https://github.com/leanprover-community/mathlib/pull/15577) analysis/inner_product_space/basic: `orthonormal` version of `linear_independent.coe_range` 
+* [PR #15470](https://github.com/leanprover-community/mathlib/pull/15470) analysis/inner_product_space/positive: definition and basic facts about positive operators 
+* [PR #14876](https://github.com/leanprover-community/mathlib/pull/14876) analysis/locally_convex/basic: a few lemmas about balanced sets 
+* [PR #15124](https://github.com/leanprover-community/mathlib/pull/15124) analysis/locally_convex/with_seminorms: in a normed space, von Neumann bounded = metric bounded 
+* [PR #15515](https://github.com/leanprover-community/mathlib/pull/15515) analysis/normed: add instances and lemmas 
+* [PR #15467](https://github.com/leanprover-community/mathlib/pull/15467) analysis/normed_space/compact_operator: definition and basic facts about compact operators 
+* [PR #15650](https://github.com/leanprover-community/mathlib/pull/15650) analysis/normed_space/linear_isometry: add defs and lemmas 
+* [PR #15471](https://github.com/leanprover-community/mathlib/pull/15471) analysis/normed_space/linear_isometry: `linear_equiv.of_eq` as a `linear_isometry_equiv` 
+* [PR #15317](https://github.com/leanprover-community/mathlib/pull/15317) analysis/normed_space/lp_space: construct star structures on lp spaces 
+* [PR #15086](https://github.com/leanprover-community/mathlib/pull/15086) analysis/normed_space/lp_space: normed_algebra structure 
+* [PR #14104](https://github.com/leanprover-community/mathlib/pull/14104) analysis/normed_space/lp_space: add l_infinity ring instances 
+* [PR #15578](https://github.com/leanprover-community/mathlib/pull/15578) analysis/normed_space/operator_norm: variant of `continuous_linear_equiv.has_sum` 
+* [PR #15417](https://github.com/leanprover-community/mathlib/pull/15417) analysis/normed_space/operator_norm: add 2 new versions of `op_norm_le_*` 
+* [PR #15173](https://github.com/leanprover-community/mathlib/pull/15173) analysis/normed_space/star/basic: make starₗᵢ apply to normed star groups 
+* [PR #15125](https://github.com/leanprover-community/mathlib/pull/15125) analysis/special_functions/complex/arg: add complex.abs_eq_one_iff 
+* [PR #14980](https://github.com/leanprover-community/mathlib/pull/14980) analysis/special_functions/complex/arg: `continuous_at_arg_coe_angle` 
+* [PR #15506](https://github.com/leanprover-community/mathlib/pull/15506) analysis/special_functions/exp: add lemmas about `is_o`/`is_O`/`is_Theta` 
+* [PR #15106](https://github.com/leanprover-community/mathlib/pull/15106) analysis/special_functions/gaussian: formula for gaussian integrals 
+* [PR #15258](https://github.com/leanprover-community/mathlib/pull/15258) analysis/special_functions/polar_coord: define polar coordinates, polar change of variable formula in integrals 
+* [PR #15164](https://github.com/leanprover-community/mathlib/pull/15164) analysis/special_functions/pow: drop an assumption in `is_o_log_rpow_rpow_at_top` 
+* [PR #15002](https://github.com/leanprover-community/mathlib/pull/15002) analysis/special_functions/pow: Rational powers are dense 
+* [PR #15651](https://github.com/leanprover-community/mathlib/pull/15651) analysis/special_functions/trigonometric/angle: equality of `cos` or `sin` 
+* [PR #14988](https://github.com/leanprover-community/mathlib/pull/14988) analysis/special_functions/trigonometric/angle: equality of twice angles 
+* [PR #15360](https://github.com/leanprover-community/mathlib/pull/15360) big_operators/fin: sum over elements of vector equal to `a` equals count `a` 
+* [PR #14422](https://github.com/leanprover-community/mathlib/pull/14422) category_theory: construction of the localized category 
+* [PR #14838](https://github.com/leanprover-community/mathlib/pull/14838) category_theory: a characterization of separating objects 
+* [PR #14974](https://github.com/leanprover-community/mathlib/pull/14974) category_theory: full_of_surjective 
+* [PR #15238](https://github.com/leanprover-community/mathlib/pull/15238) category_theory: a category with a small detecting set is well-powered 
+* [PR #15377](https://github.com/leanprover-community/mathlib/pull/15377) category_theory: limits of essentially small indexing categories 
+* [PR #14880](https://github.com/leanprover-community/mathlib/pull/14880) category_theory: (co)products and (co)separators 
+* [PR #14026](https://github.com/leanprover-community/mathlib/pull/14026) category_theory: left-exact functors preserve finite limits 
+* [PR #15121](https://github.com/leanprover-community/mathlib/pull/15121) category_theory//algebra: epi_of_epi and mono_of_mono 
+* [PR #14581](https://github.com/leanprover-community/mathlib/pull/14581) category_theory/abelian/: functors that preserve finite limits and colimits preserve exactness 
+* [PR #14834](https://github.com/leanprover-community/mathlib/pull/14834) category_theory/endofunctor/algebra: Define coalgebras over an endofunctor and prove an equivalence 
+* [PR #14829](https://github.com/leanprover-community/mathlib/pull/14829) category_theory/functor: preserving/reflecting monos/epis 
+* [PR #14419](https://github.com/leanprover-community/mathlib/pull/14419) category_theory/limits: preserves biproducts if comparison is iso 
+* [PR #14526](https://github.com/leanprover-community/mathlib/pull/14526) category_theory/limits: opposites of limit pullback cones 
+* [PR #14452](https://github.com/leanprover-community/mathlib/pull/14452) category_theory/limits: bilimit from kernel 
+* [PR #14948](https://github.com/leanprover-community/mathlib/pull/14948) category_theory/limits/construction: Construct finite limits from terminal objects and pullbacks 
+* [PR #15269](https://github.com/leanprover-community/mathlib/pull/15269) category_theory/limits/shapes/comm_sq: opposites of is_pullback and is_pushout 
+* [PR #14445](https://github.com/leanprover-community/mathlib/pull/14445) category_theory/preadditive: constructing a semiadditive structure from binary biproducts 
+* [PR #15096](https://github.com/leanprover-community/mathlib/pull/15096) category_theory/preadditive: left exactness of certain hom functors 
+* [PR #14832](https://github.com/leanprover-community/mathlib/pull/14832) category_theory/preadditive: projective iff coyoneda.obj preserves epimorphisms 
+* [PR #15100](https://github.com/leanprover-community/mathlib/pull/15100) category_theory/preadditive: algebra over endofunctor preadditive and forget additive functor 
+* [PR #15455](https://github.com/leanprover-community/mathlib/pull/15455) category_theory/shapes/pullbacks: Pullbacks isomorphic to the opposite of pushouts 
+* [PR #14831](https://github.com/leanprover-community/mathlib/pull/14831) category_theory/yoneda: coyoneda.obj_op_op 
+* [PR #15327](https://github.com/leanprover-community/mathlib/pull/15327) combinatorics/additive/behrend: Behrend's lower bound on Roth numbers 
+* [PR #14070](https://github.com/leanprover-community/mathlib/pull/14070) combinatorics/additive/behrend: Behrend's construction 
+* [PR #14697](https://github.com/leanprover-community/mathlib/pull/14697) combinatorics/additive/ruzsa_covering: The Ruzsa covering lemma 
+* [PR #14497](https://github.com/leanprover-community/mathlib/pull/14497) combinatorics/set_family/harris_kleitman: The Harris-Kleitman inequality 
+* [PR #14475](https://github.com/leanprover-community/mathlib/pull/14475) combinatorics/set_family/intersecting: Intersecting families 
+* [PR #14543](https://github.com/leanprover-community/mathlib/pull/14543) combinatorics/set_family/kleitman: Kleitman's bound 
+* [PR #15150](https://github.com/leanprover-community/mathlib/pull/15150) combinatorics/simple_graph/basic: `dart.to_prod` is injective 
+* [PR #15156](https://github.com/leanprover-community/mathlib/pull/15156) combinatorics/simple_graph/connectivity: operations and lemmas about path type 
+* [PR #15153](https://github.com/leanprover-community/mathlib/pull/15153) combinatorics/simple_graph/connectivity: simp confluence 
+* [PR #15353](https://github.com/leanprover-community/mathlib/pull/15353) combinatorics/simple_graph/density: Bound on the difference between edge densities 
+* [PR #14978](https://github.com/leanprover-community/mathlib/pull/14978) combinatorics/simple_graph/hasse: The Hasse diagram of `α × β` 
+* [PR #14867](https://github.com/leanprover-community/mathlib/pull/14867) combinatorics/simple_graph/prod: Box product 
+* [PR #13222](https://github.com/leanprover-community/mathlib/pull/13222) combinatorics/simple_graph/regularity/equitabilise: Equitabilising a partition 
+* [PR #14403](https://github.com/leanprover-community/mathlib/pull/14403) combinatorics/simple_graph/subgraph: delete vertices in a subgraph 
+* [PR #14877](https://github.com/leanprover-community/mathlib/pull/14877) combinatorics/simple_graph/subgraph: add `subgraph.comap` and subgraph of subgraph coercion 
+* [PR #15158](https://github.com/leanprover-community/mathlib/pull/15158) combinatorics/simple_graph/trails: Euler's condition for trails  
+* [PR #14034](https://github.com/leanprover-community/mathlib/pull/14034) combinatorics/simple_graph/{basic,subgraph,clique,coloring}: add induced graphs, characterization of cliques, and bounds for colorings 
+* [PR #15505](https://github.com/leanprover-community/mathlib/pull/15505) computability/ackermann: the Ackermann function isn't primitive recursive 
+* [PR #15280](https://github.com/leanprover-community/mathlib/pull/15280) data/countable: add `countable` typeclass 
+* [PR #15337](https://github.com/leanprover-community/mathlib/pull/15337) data/fin/basic: add a reflected instance 
+* [PR #15048](https://github.com/leanprover-community/mathlib/pull/15048) data/fin/tuple/basic: add lemmas for rewriting exists and forall over `n+1`-tuples 
+* [PR #15607](https://github.com/leanprover-community/mathlib/pull/15607) data/finset/basic: There is exactly one set in empty types 
+* [PR #15385](https://github.com/leanprover-community/mathlib/pull/15385) data/finset/basic: lemmas about `filter`, `cons`, and `disj_union` 
+* [PR #15170](https://github.com/leanprover-community/mathlib/pull/15170) data/finset/basic: Add `decidable_nonempty` for finsets. 
+* [PR #15011](https://github.com/leanprover-community/mathlib/pull/15011) data/finset/basic: Coercion of a product of finsets 
+* [PR #15257](https://github.com/leanprover-community/mathlib/pull/15257) data/finset/fold: add lemma `fold_max_add` 
+* [PR #15212](https://github.com/leanprover-community/mathlib/pull/15212) data/finset/lattice: add three.2 lemmas about `finset.max/min` 
+* [PR #15435](https://github.com/leanprover-community/mathlib/pull/15435) data/finset/pointwise: Singleton arithmetic 
+* [PR #15387](https://github.com/leanprover-community/mathlib/pull/15387) data/finset/powerset: More `powerset` lemmas 
+* [PR #15197](https://github.com/leanprover-community/mathlib/pull/15197) data/finsupp/basic: graph of a finitely supported function 
+* [PR #15155](https://github.com/leanprover-community/mathlib/pull/15155) data/finsupp/big_operators: sum of finsupp and their support 
+* [PR #15080](https://github.com/leanprover-community/mathlib/pull/15080) data/fintype/basic: add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. 
+* [PR #15207](https://github.com/leanprover-community/mathlib/pull/15207) data/json: helper functions for json serialization 
+* [PR #15138](https://github.com/leanprover-community/mathlib/pull/15138) data/list: accessing list with fallback 
+* [PR #15472](https://github.com/leanprover-community/mathlib/pull/15472) data/list/basic: when drop_while and take_while hold 
+* [PR #15482](https://github.com/leanprover-community/mathlib/pull/15482) data/list/basic: last_reverse 
+* [PR #15139](https://github.com/leanprover-community/mathlib/pull/15139) data/list/basic: nth_le_enum 
+* [PR #14777](https://github.com/leanprover-community/mathlib/pull/14777) data/list/basic: add filter_map_join 
+* [PR #15473](https://github.com/leanprover-community/mathlib/pull/15473) data/list/infix: drop_while and take_while suf/prefix 
+* [PR #15433](https://github.com/leanprover-community/mathlib/pull/15433) data/list/of_fn: lemmas to turn quantifiers over lists to quantifiers over tuples 
+* [PR #15386](https://github.com/leanprover-community/mathlib/pull/15386) data/matrix/basic: Add `alg_equiv` and `linear_equiv` instances for transpose. 
+* [PR #14991](https://github.com/leanprover-community/mathlib/pull/14991) data/matrix/notation: add `!![1, 2; 3, 4]` notation 
+* [PR #15094](https://github.com/leanprover-community/mathlib/pull/15094) data/multiset/fintype: coercion from multiset to type 
+* [PR #15457](https://github.com/leanprover-community/mathlib/pull/15457) data/nat/basic: add recursion principle `even_odd_rec` as a wrapper around `binary_rec` 
+* [PR #15061](https://github.com/leanprover-community/mathlib/pull/15061) data/nat/basic: add `strong_sub_recursion` and `pincer_recursion` 
+* [PR #15099](https://github.com/leanprover-community/mathlib/pull/15099) data/nat/basic: split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas 
+* [PR #15031](https://github.com/leanprover-community/mathlib/pull/15031) data/nat/basic: add `mul_div_mul_comm_of_dvd_dvd` 
+* [PR #15409](https://github.com/leanprover-community/mathlib/pull/15409) data/nat/bitwise: tweak `lxor` lemmas 
+* [PR #15072](https://github.com/leanprover-community/mathlib/pull/15072) data/nat/choose/basic: Definition of `multichoose` and basic lemmas 
+* [PR #15029](https://github.com/leanprover-community/mathlib/pull/15029) data/nat/enat: simple lemmas on `enat` 
+* [PR #15767](https://github.com/leanprover-community/mathlib/pull/15767) data/nat/factorization/basic: add lemma `prime.factorization_self` 
+* [PR #15277](https://github.com/leanprover-community/mathlib/pull/15277) data/nat/factorization/basic: golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` 
+* [PR #15014](https://github.com/leanprover-community/mathlib/pull/15014) data/nat/factorization/basic: add lemma `factorization_eq_card_pow_dvd` 
+* [PR #15539](https://github.com/leanprover-community/mathlib/pull/15539) data/nat/pairing: basic bounds on `mkpair` 
+* [PR #15268](https://github.com/leanprover-community/mathlib/pull/15268) data/nat/parity: `nat.bit1_div_bit0` 
+* [PR #15645](https://github.com/leanprover-community/mathlib/pull/15645) data/nat/totient: lemmas `totient_mul_of_prime_of_{not_}dvd` 
+* [PR #15313](https://github.com/leanprover-community/mathlib/pull/15313) data/pfun: tooling to help reasoning about pfun domains 
+* [PR #15588](https://github.com/leanprover-community/mathlib/pull/15588) data/pi/algebra: sum_elim lemmas 
+* [PR #15508](https://github.com/leanprover-community/mathlib/pull/15508) data/pnat/basic: add lemmas, move `equiv.pnat_equiv_nat` 
+* [PR #15183](https://github.com/leanprover-community/mathlib/pull/15183) data/pnat/basic: `succ` as an order isomorphism between `ℕ` and `ℕ+` 
+* [PR #15199](https://github.com/leanprover-community/mathlib/pull/15199) data/polynomial/degree/definitions: redefine `polynomial.degree` as `p.support.max` 
+* [PR #15522](https://github.com/leanprover-community/mathlib/pull/15522) data/polynomial/degree/lemmas: three lemmas on nat_degrees, bits and neg 
+* [PR #14741](https://github.com/leanprover-community/mathlib/pull/14741) data/polynomial/erase_lead: Characterization of polynomials of fixed support 
+* [PR #15225](https://github.com/leanprover-community/mathlib/pull/15225) data/polynomial/laurent: define `degree` and some API 
+* [PR #15318](https://github.com/leanprover-community/mathlib/pull/15318) data/polynomial/unit_trinomial: Irreducibility of X^n-X-1 
+* [PR #14914](https://github.com/leanprover-community/mathlib/pull/14914) data/polynomial/unit_trinomial: An irreducibility criterion for unit trinomials 
+* [PR #15148](https://github.com/leanprover-community/mathlib/pull/15148) data/quot: `is_equiv` instance for quotient equivalence 
+* [PR #15101](https://github.com/leanprover-community/mathlib/pull/15101) data/rat/defs: add denominator as pnat 
+* [PR #15575](https://github.com/leanprover-community/mathlib/pull/15575) data/real/basic: add a repr showing an underlying cauchy sequence 
+* [PR #15483](https://github.com/leanprover-community/mathlib/pull/15483) data/real/{e,}nnreal: images and preimages of `ord_connected` sets 
+* [PR #14970](https://github.com/leanprover-community/mathlib/pull/14970) data/set/basic,order/filter/basic: add semiconj lemmas about images and maps 
+* [PR #15671](https://github.com/leanprover-community/mathlib/pull/15671) data/set/countable: add `iff` versions of some lemmas 
+* [PR #15415](https://github.com/leanprover-community/mathlib/pull/15415) data/set/countable: protect lemmas 
+* [PR #15444](https://github.com/leanprover-community/mathlib/pull/15444) data/set/finite: set.finite.induction_on' 
+* [PR #15177](https://github.com/leanprover-community/mathlib/pull/15177) data/set/finite: add `multiset.finite_to_set` 
+* [PR #15605](https://github.com/leanprover-community/mathlib/pull/15605) data/set/function: add lemmas about `set.restrict` 
+* [PR #15608](https://github.com/leanprover-community/mathlib/pull/15608) data/set/intervals: add lemmas 
+* [PR #14928](https://github.com/leanprover-community/mathlib/pull/14928) data/set/pointwise: `list` and `multiset` versions of n-ary lemmas 
+* [PR #15604](https://github.com/leanprover-community/mathlib/pull/15604) data/set/prod: add theorems about `λ x, (x, x)` 
+* [PR #15652](https://github.com/leanprover-community/mathlib/pull/15652) data/sign: `left.sign_neg`, `right.sign_neg` 
+* [PR #15358](https://github.com/leanprover-community/mathlib/pull/15358) data/sum/basic: `sum.lift_rel` is a subrelation of `sum.lex` 
+* [PR #15370](https://github.com/leanprover-community/mathlib/pull/15370) data/sum/order: `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` 
+* [PR #15192](https://github.com/leanprover-community/mathlib/pull/15192) data/sym/basic: combinatorial equivalence for `sym (option α) n.succ` 
+* [PR #11162](https://github.com/leanprover-community/mathlib/pull/11162) data/sym/card: Prove stars and bars 
+* [PR #15383](https://github.com/leanprover-community/mathlib/pull/15383) data/vector/basic: make the recursor work with `induction _ using` syntax 
+* [PR #15154](https://github.com/leanprover-community/mathlib/pull/15154) data/vector/mem: Lemmas about membership in a vector 
+* [PR #15493](https://github.com/leanprover-community/mathlib/pull/15493) data/{finset,set}/basic: `insert a s = s ↔ a ∈ s` 
+* [PR #15478](https://github.com/leanprover-community/mathlib/pull/15478) data/{pi, prod}: add missing `has_pow` instances for `pi` type 
+* [PR #15724](https://github.com/leanprover-community/mathlib/pull/15724) field_theory/adjoin: A compositum of algebraic extensions is algebraic 
+* [PR #15426](https://github.com/leanprover-community/mathlib/pull/15426) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version 
+* [PR #15518](https://github.com/leanprover-community/mathlib/pull/15518) field_theory/adjoin: `intermediate_field.exists_finset_of_mem_supr` 
+* [PR #15438](https://github.com/leanprover-community/mathlib/pull/15438) field_theory/adjoin: Compact elements of `intermediate_field` 
+* [PR #15420](https://github.com/leanprover-community/mathlib/pull/15420) field_theory/adjoin: `F⟮α⟯ ≤ K ↔ α ∈ K` 
+* [PR #15339](https://github.com/leanprover-community/mathlib/pull/15339) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional 
+* [PR #15659](https://github.com/leanprover-community/mathlib/pull/15659) field_theory/intermediate_field: Produce an intermediate field from a subalgebra satisfying `is_field`. 
+* [PR #15188](https://github.com/leanprover-community/mathlib/pull/15188) field_theory/intermediate_field: `dsimp` lemma 
+* [PR #15303](https://github.com/leanprover-community/mathlib/pull/15303) field_theory/tower: if `L / K / F` is finite, so is `K / F` 
+* [PR #15021](https://github.com/leanprover-community/mathlib/pull/15021) geometry/euclidean/basic: `continuous_at_angle` 
+* [PR #15463](https://github.com/leanprover-community/mathlib/pull/15463) geometry/euclidean/oriented_angle: `continuous_at_oangle` 
+* [PR #15560](https://github.com/leanprover-community/mathlib/pull/15560) geometry/manifold: generalize some lemmas from `smooth` to `cont_mdiff` 
+* [PR #15116](https://github.com/leanprover-community/mathlib/pull/15116) geometry/manifold/local_invariant_properties: simplify definitions and proofs 
+* [PR #15437](https://github.com/leanprover-community/mathlib/pull/15437) geometry/manifold/metrizable: metrizability of a manifold 
+* [PR #15314](https://github.com/leanprover-community/mathlib/pull/15314) geometry/manifold|topology: add simps and ext attributes 
+* [PR #14182](https://github.com/leanprover-community/mathlib/pull/14182) group_theory/complement: transversal for the transfer homomorphism 
+* [PR #15402](https://github.com/leanprover-community/mathlib/pull/15402) group_theory/finite_abelian: a finitely generated torsion abelian group is finite 
+* [PR #15239](https://github.com/leanprover-community/mathlib/pull/15239) group_theory/group_action/option: Scalar action on an option 
+* [PR #15050](https://github.com/leanprover-community/mathlib/pull/15050) group_theory/group_action/sub_mul_action: add the pointwise monoid structure 
+* [PR #8632](https://github.com/leanprover-community/mathlib/pull/8632) group_theory/p_group: Groups of order p^2 are commutative 
+* [PR #15052](https://github.com/leanprover-community/mathlib/pull/15052) group_theory/submonoid/pointwise: add the pointwise monoid structure on `add_submonoid` 
+* [PR #13945](https://github.com/leanprover-community/mathlib/pull/13945) group_theory/subsemigroup/membership: add membership criteria for subsemigroups 
+* [PR #14739](https://github.com/leanprover-community/mathlib/pull/14739) information_theory/hamming: add Hamming distance and norm 
+* [PR #15603](https://github.com/leanprover-community/mathlib/pull/15603) integration: elementary version of FTC-1 
+* [PR #15587](https://github.com/leanprover-community/mathlib/pull/15587) linear_algebra: lemmas on associatedness of determinants of linear maps 
+* [PR #15119](https://github.com/leanprover-community/mathlib/pull/15119) linear_algebra: basis on R × R, and relation between matrices and linear maps in this basis  
+* [PR #14714](https://github.com/leanprover-community/mathlib/pull/14714) linear_algebra: add lemma `linear_independent.finite_of_is_noetherian` 
+* [PR #12140](https://github.com/leanprover-community/mathlib/pull/12140) linear_algebra/annihilating_polynomial: add definition of annihilating ideal and show minpoly generates in field case 
+* [PR #14883](https://github.com/leanprover-community/mathlib/pull/14883) linear_algebra/basis: shows the lattice of submodules of a module over a division ring is atomistic 
+* [PR #14790](https://github.com/leanprover-community/mathlib/pull/14790) linear_algebra/clifford_algebra/even: Universal property and isomorphisms for the even subalgebra 
+* [PR #15558](https://github.com/leanprover-community/mathlib/pull/15558) linear_algebra/finite_dimensional: One-dimensional iff principal 
+* [PR #15531](https://github.com/leanprover-community/mathlib/pull/15531) linear_algebra/linear_pmap: more lemmas about the graph 
+* [PR #14922](https://github.com/leanprover-community/mathlib/pull/14922) linear_algebra/linear_pmap: construct a `linear_pmap` from its graph 
+* [PR #14794](https://github.com/leanprover-community/mathlib/pull/14794) linear_algebra/matrix: inner prod of matrix 
+* [PR #15459](https://github.com/leanprover-community/mathlib/pull/15459) linear_algebra/matrix/charpoly: Coefficients of the characteristic polynomial falls in the ideal power. 
+* [PR #15391](https://github.com/leanprover-community/mathlib/pull/15391) linear_algebra/projective_space/subspace: defines subspaces of a projective space 
+* [PR #14542](https://github.com/leanprover-community/mathlib/pull/14542) linear_algebra/projectivization/independence: defines (in)dependence of points in projective space 
+* [PR #15628](https://github.com/leanprover-community/mathlib/pull/15628) linear_algebra/tensor_product: add id_apply and comp_apply for ltensor and rtensor 
+* [PR #15209](https://github.com/leanprover-community/mathlib/pull/15209) linear_algebra/unitary_group: better constructor 
+* [PR #15524](https://github.com/leanprover-community/mathlib/pull/15524) logic/encodable/basic: an encodable type is countable 
+* [PR #15611](https://github.com/leanprover-community/mathlib/pull/15611) logic/equiv/local_equiv: add 2 lemmas 
+* [PR #15176](https://github.com/leanprover-community/mathlib/pull/15176) logic/equiv/set: define `equiv.set.pi` 
+* [PR #15574](https://github.com/leanprover-community/mathlib/pull/15574) logic/nonempty: `pi.nonempty` instance 
+* [PR #15307](https://github.com/leanprover-community/mathlib/pull/15307) measure_theory/constructions/borel_space: the set of points for which a measurable sequence of functions converges is measurable 
+* [PR #14424](https://github.com/leanprover-community/mathlib/pull/14424) measure_theory/constructions/prod: The layercake integral. 
+* [PR #15422](https://github.com/leanprover-community/mathlib/pull/15422) measure_theory/function/conditional_expecation: conditional expectation of a function to a independent sigma-algebra  
+* [PR #15274](https://github.com/leanprover-community/mathlib/pull/15274) measure_theory/function/conditional_expectation: pull-out property of the conditional expectation 
+* [PR #15024](https://github.com/leanprover-community/mathlib/pull/15024) measure_theory/function/conditional_expectation: monotonicity of the conditional expectation 
+* [PR #15378](https://github.com/leanprover-community/mathlib/pull/15378) measure_theory/function/uniform_integrable: conditional expectations form a uniformly integrable class 
+* [PR #15120](https://github.com/leanprover-community/mathlib/pull/15120) measure_theory/group/measure: a product of Haar measures is a Haar measure 
+* [PR #15423](https://github.com/leanprover-community/mathlib/pull/15423) measure_theory/integral: generalize some integral properties to set_to_fun 
+* [PR #13885](https://github.com/leanprover-community/mathlib/pull/13885) measure_theory/integral: Circle integral transform 
+* [PR #15344](https://github.com/leanprover-community/mathlib/pull/15344) measure_theory/integral/set_integral: add `set_integral_indicator` 
+* [PR #15342](https://github.com/leanprover-community/mathlib/pull/15342) measure_theory/measurable_space_def: add `generate_from_induction` 
+* [PR #15528](https://github.com/leanprover-community/mathlib/pull/15528) measure_theory/measure/finite_measure_weak_convergence: Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. 
+* [PR #15205](https://github.com/leanprover-community/mathlib/pull/15205) measure_theory/measure/finite_measure_weak_convergence: Add some missing API lemmas. 
+* [PR #15343](https://github.com/leanprover-community/mathlib/pull/15343) measure_theory/measure/measure_space: generalize measure.comap 
+* [PR #15066](https://github.com/leanprover-community/mathlib/pull/15066) measure_theory/pmf: lawful monad instance for probability mass function monad 
+* [PR #8002](https://github.com/leanprover-community/mathlib/pull/8002) number_theory: Bertrand's postulate, slightly different approach 
+* [PR #15315](https://github.com/leanprover-community/mathlib/pull/15315) number_theory: degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` 
+* [PR #15418](https://github.com/leanprover-community/mathlib/pull/15418) number_theory/legendre_symbol/: redefine quadratic characters as `mul_char`s 
+* [PR #15499](https://github.com/leanprover-community/mathlib/pull/15499) number_theory/legendre_symbol/add_character: add file introducing additive characters 
+* [PR #15007](https://github.com/leanprover-community/mathlib/pull/15007) number_theory/slash_actions: Slash actions class for modular forms 
+* [PR #14717](https://github.com/leanprover-community/mathlib/pull/14717) number_theory/wilson: add Wilson's Theorem 
+* [PR #15149](https://github.com/leanprover-community/mathlib/pull/15149) order/basic: a symmetric relation implies equality when it implies less-equal 
+* [PR #15606](https://github.com/leanprover-community/mathlib/pull/15606) order/boolean_algebra: A bounded generalized boolean algebra is a boolean algebra 
+* [PR #15278](https://github.com/leanprover-community/mathlib/pull/15278) order/bounded_order: `is_well_order` instances for `with_top` and `with_bot` 
+* [PR #15636](https://github.com/leanprover-community/mathlib/pull/15636) order/bounded_order: an order is either an `order_bot` or a `no_bot_order` 
+* [PR #15341](https://github.com/leanprover-community/mathlib/pull/15341) order/bounded_order: two lemmas about the interaction between monotonicity and map with_bot/top 
+* [PR #15357](https://github.com/leanprover-community/mathlib/pull/15357) order/bounded_order: `subrelation r s ↔ r ≤ s` 
+* [PR #14195](https://github.com/leanprover-community/mathlib/pull/14195) order/bounded_order: Codisjointness 
+* [PR #15665](https://github.com/leanprover-community/mathlib/pull/15665) order/compare: general cleanup 
+* [PR #15340](https://github.com/leanprover-community/mathlib/pull/15340) order/complete_boolean_algebra: A frame is distributive 
+* [PR #15237](https://github.com/leanprover-community/mathlib/pull/15237) order/filter: add `map_neg_at_top`, change some assumptions 
+* [PR #15632](https://github.com/leanprover-community/mathlib/pull/15632) order/filter: `filter.pi` is countably generated 
+* [PR #15630](https://github.com/leanprover-community/mathlib/pull/15630) order/filter/bases: lemmas about bases of product filters 
+* [PR #15661](https://github.com/leanprover-community/mathlib/pull/15661) order/filter/basic: add `filter.has_basis.bInter_mem` 
+* [PR #15128](https://github.com/leanprover-community/mathlib/pull/15128) order/filter/basic: add `map_le_map` and `map_injective` 
+* [PR #15187](https://github.com/leanprover-community/mathlib/pull/15187) order/filter/ultrafilter: `pure`, `map`, and `comap` lemmas 
+* [PR #15432](https://github.com/leanprover-community/mathlib/pull/15432) order/hom/basic: `order_iso` of `rel_iso (<) (<)` 
+* [PR #15182](https://github.com/leanprover-community/mathlib/pull/15182) order/hom/basic: `order_iso` to `rel_iso (<) (<)` 
+* [PR #15375](https://github.com/leanprover-community/mathlib/pull/15375) order/initial_seg: Initial/principal segment from empty type 
+* [PR #15374](https://github.com/leanprover-community/mathlib/pull/15374) order/initial_seg: remove `nolint` from `initial_seg` 
+* [PR #15439](https://github.com/leanprover-community/mathlib/pull/15439) order/lattice: Congruence lemmas for `⊔` and `⊓` 
+* [PR #14789](https://github.com/leanprover-community/mathlib/pull/14789) order/lattice, data/set: some helper lemmas 
+* [PR #15136](https://github.com/leanprover-community/mathlib/pull/15136) order/lattice, order/lattice_intervals: coe inf/sup lemmas 
+* [PR #14733](https://github.com/leanprover-community/mathlib/pull/14733) order/locally_finite: make `fintype.to_locally_finite_order` computable 
+* [PR #11602](https://github.com/leanprover-community/mathlib/pull/11602) order/modular_lattice: Semimodular lattices 
+* [PR #15073](https://github.com/leanprover-community/mathlib/pull/15073) order/order_iso_nat: generalize `well_founded.monotone_chain_condition` to preorders 
+* [PR #15350](https://github.com/leanprover-community/mathlib/pull/15350) order/partition/finpartition: Bound size of a bit of `finpartition.atomise` 
+* [PR #15430](https://github.com/leanprover-community/mathlib/pull/15430) order/rel_iso: add lemmas on `rel_iso.cast` 
+* [PR #15372](https://github.com/leanprover-community/mathlib/pull/15372) order/rel_iso: relation embedding from empty type 
+* [PR #14760](https://github.com/leanprover-community/mathlib/pull/14760) order/rel_iso: two reflexive/irreflexive relations on a unique type are isomorphic 
+* [PR #15144](https://github.com/leanprover-community/mathlib/pull/15144) order/rel_iso: add `rel_iso.cast` 
+* [PR #15016](https://github.com/leanprover-community/mathlib/pull/15016) order/succ_pred: expand API on `with_bot` and `with_top` 
+* [PR #15567](https://github.com/leanprover-community/mathlib/pull/15567) order/succ_pred/basic: `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related 
+* [PR #15536](https://github.com/leanprover-community/mathlib/pull/15536) order/succ_pred/basic: `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses 
+* [PR #15001](https://github.com/leanprover-community/mathlib/pull/15001) order/succ_pred/limit: Successor and predecessor limits 
+* [PR #15581](https://github.com/leanprover-community/mathlib/pull/15581) order/upper_lower: Upper closure of a set 
+* [PR #15399](https://github.com/leanprover-community/mathlib/pull/15399) order/well_founded: typeclasses for well-founded `<` and `>` 
+* [PR #15266](https://github.com/leanprover-community/mathlib/pull/15266) order/well_founded_set: any relation is well-founded on `Ø` 
+* [PR #15678](https://github.com/leanprover-community/mathlib/pull/15678) probability/density: probability of event in uniform distribution 
+* [PR #15131](https://github.com/leanprover-community/mathlib/pull/15131) probability/independence: two tuples indexed by disjoint subsets of an independent family of r.v. are independent 
+* [PR #14909](https://github.com/leanprover-community/mathlib/pull/14909) probability/martingale: the discrete stochastic integral of a submartingale is a submartingale 
+* [PR #14737](https://github.com/leanprover-community/mathlib/pull/14737) probability/martingale: Doob's maximal inequality 
+* [PR #14932](https://github.com/leanprover-community/mathlib/pull/14932) probability/martingale: positive part of a submartingale is also a submartingale 
+* [PR #15140](https://github.com/leanprover-community/mathlib/pull/15140) probability/moments: mgf/cgf of a sum of independent random variables 
+* [PR #15129](https://github.com/leanprover-community/mathlib/pull/15129) probability/moments: Chernoff bound on the upper/lower tail of a real random variable 
+* [PR #15392](https://github.com/leanprover-community/mathlib/pull/15392) probability/strong_law: Lp version of the strong law of large numbers 
+* [PR #14331](https://github.com/leanprover-community/mathlib/pull/14331) representation_theory/Action: mapping by a monoidal functor 
+* [PR #13713](https://github.com/leanprover-community/mathlib/pull/13713) representation_theory/Rep: Rep k G ≌ Module (monoid_algebra k G) 
+* [PR #15084](https://github.com/leanprover-community/mathlib/pull/15084) representation_theory/character: formula for the dimension of the invariants in terms of the character 
+* [PR #14308](https://github.com/leanprover-community/mathlib/pull/14308) representation_theory/monoid_algebra_basis: add some API for `k[G^n]` 
+* [PR #15243](https://github.com/leanprover-community/mathlib/pull/15243) ring_theory: Formally étale/smooth/unramified morphisms are stable under base change. 
+* [PR #14348](https://github.com/leanprover-community/mathlib/pull/14348) ring_theory: the Ore localization of a ring 
+* [PR #15381](https://github.com/leanprover-community/mathlib/pull/15381) ring_theory: the integral closure `C` of `A` is Noetherian over `A` 
+* [PR #14966](https://github.com/leanprover-community/mathlib/pull/14966) ring_theory: Basic framework for classes of ring homomorphisms 
+* [PR #15064](https://github.com/leanprover-community/mathlib/pull/15064) ring_theory: Some missing lemmas 
+* [PR #15333](https://github.com/leanprover-community/mathlib/pull/15333) ring_theory/I_filtration: I-filtrations of modules. 
+* [PR #14981](https://github.com/leanprover-community/mathlib/pull/14981) ring_theory/adjoin_root: add lemmas for GCD domains 
+* [PR #15586](https://github.com/leanprover-community/mathlib/pull/15586) ring_theory/algebraic: `is_algebraic_algebra_map_iff` 
+* [PR #15424](https://github.com/leanprover-community/mathlib/pull/15424) ring_theory/bezout: Bezout domains are integrally closed 
+* [PR #15091](https://github.com/leanprover-community/mathlib/pull/15091) ring_theory/bezout: Define Bézout rings. 
+* [PR #11053](https://github.com/leanprover-community/mathlib/pull/11053) ring_theory/dedekind_domain: If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape 
+* [PR #15244](https://github.com/leanprover-community/mathlib/pull/15244) ring_theory/derivation: Derivations into square-zero ideals corresponds to liftings.  
+* [PR #15242](https://github.com/leanprover-community/mathlib/pull/15242) ring_theory/etale: Formally étale morphisms. 
+* [PR #15264](https://github.com/leanprover-community/mathlib/pull/15264) ring_theory/graded_algebra/basic: add lemma `proj_homogeneous_mul` 
+* [PR #15460](https://github.com/leanprover-community/mathlib/pull/15460) ring_theory/ideal/operations: A variant of `finsupp.total` for ideals. 
+* [PR #12812](https://github.com/leanprover-community/mathlib/pull/12812) ring_theory/integrally_closed: if x is in Frac R such that x^n is in R then x is in R 
+* [PR #15404](https://github.com/leanprover-community/mathlib/pull/15404) ring_theory/localization/basic: section of localisation of non-zero is non-zero 
+* [PR #15261](https://github.com/leanprover-community/mathlib/pull/15261) ring_theory/localization/basic: add `mk_sum` 
+* [PR #15561](https://github.com/leanprover-community/mathlib/pull/15561) ring_theory/noetherian: Finitely generated idempotent ideal is principal. 
+* [PR #15397](https://github.com/leanprover-community/mathlib/pull/15397) ring_theory/power_series/basic: Add `rescale_X` 
+* [PR #15287](https://github.com/leanprover-community/mathlib/pull/15287) ring_theory/power_series/well_known: Coefficients of sin and cos 
+* [PR #15089](https://github.com/leanprover-community/mathlib/pull/15089) ring_theory/rees_algebra: Define the Rees algebra of an ideal. 
+* [PR #15427](https://github.com/leanprover-community/mathlib/pull/15427) ring_theory/ring_hom/finite: Finite ring morphisms are stable under base change 
+* [PR #15379](https://github.com/leanprover-community/mathlib/pull/15379) ring_theory/ring_hom/finite: Finite type is a local property 
+* [PR #15512](https://github.com/leanprover-community/mathlib/pull/15512) ring_theory/tensor_product: A predicate for being the tensor product. 
+* [PR #15241](https://github.com/leanprover-community/mathlib/pull/15241) ring_theory/tensor_product: `A`-algebra structure on `A' ⊗[R] B`. 
+* [PR #15093](https://github.com/leanprover-community/mathlib/pull/15093) ring_theory/valuation: Properties of valuation rings. 
+* [PR #14896](https://github.com/leanprover-community/mathlib/pull/14896) set/intervals/monotone: add some monotonicity lemmas 
+* [PR #14989](https://github.com/leanprover-community/mathlib/pull/14989) set_theory/cardinal/ordinal: basic properties on Beth numbers 
+* [PR #15198](https://github.com/leanprover-community/mathlib/pull/15198) set_theory/cardinal/ordinal: cardinality of `α →₀ β` 
+* [PR #15367](https://github.com/leanprover-community/mathlib/pull/15367) set_theory/game/nim: make the file `noncomputable theory` 
+* [PR #14780](https://github.com/leanprover-community/mathlib/pull/14780) set_theory/game/ordinal: lemmas on `0.to_pgame` and `1.to_pgame` 
+* [PR #15255](https://github.com/leanprover-community/mathlib/pull/15255) set_theory/game/pgame: strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` 
+* [PR #15256](https://github.com/leanprover-community/mathlib/pull/15256) set_theory/game/pgame: `is_option (-x) (-y) ↔ is_option x y` 
+* [PR #15254](https://github.com/leanprover-community/mathlib/pull/15254) set_theory/game/pgame: add `equiv.comm` 
+* [PR #15533](https://github.com/leanprover-community/mathlib/pull/15533) set_theory/ordinal/arithmetic: `pred 0 = 0` 
+* [PR #15447](https://github.com/leanprover-community/mathlib/pull/15447) set_theory/ordinal/arithmetic: more log lemmas 
+* [PR #15193](https://github.com/leanprover-community/mathlib/pull/15193) set_theory/ordinal/arithmetic: tweak `type_add` and `type_mul` 
+* [PR #15174](https://github.com/leanprover-community/mathlib/pull/15174) set_theory/ordinal/arithmetic: tweak theorems about `0` and `1` 
+* [PR #15348](https://github.com/leanprover-community/mathlib/pull/15348) set_theory/ordinal/basic: dot notation lemmas + golf 
+* [PR #15152](https://github.com/leanprover-community/mathlib/pull/15152) set_theory/ordinal/basic: add `gc_ord_card` and `gci_ord_card` 
+* [PR #15194](https://github.com/leanprover-community/mathlib/pull/15194) set_theory/ordinal/basic: mark `type_fintype` as `simp` 
+* [PR #15178](https://github.com/leanprover-community/mathlib/pull/15178) set_theory/ordinal/basic: order type of naturals is `ω` 
+* [PR #15146](https://github.com/leanprover-community/mathlib/pull/15146) set_theory/ordinal/basic: basic lemmas on `ordinal.lift`  
+* [PR #15320](https://github.com/leanprover-community/mathlib/pull/15320) set_theory/zfc: ZFC sets are small types 
+* [PR #15223](https://github.com/leanprover-community/mathlib/pull/15223) set_theory/zfc: `Ø ⊆ x` 
+* [PR #15213](https://github.com/leanprover-community/mathlib/pull/15213) set_theory/zfc: `∈` is well-founded 
+* [PR #15324](https://github.com/leanprover-community/mathlib/pull/15324) set_theory/zfc: more `quotient` lemmas 
+* [PR #15214](https://github.com/leanprover-community/mathlib/pull/15214) set_theory/zfc: simp lemmas for `arity` and `const` 
+* [PR #15211](https://github.com/leanprover-community/mathlib/pull/15211) set_theory/zfc: basic lemmas on `pSet.equiv` 
+* [PR #15545](https://github.com/leanprover-community/mathlib/pull/15545) set_theory/zfc/basic: `inj` lemmas 
+* [PR #15544](https://github.com/leanprover-community/mathlib/pull/15544) set_theory/zfc/basic: `∈` is well-founded on classes 
+* [PR #15573](https://github.com/leanprover-community/mathlib/pull/15573) set_theory/zfc/basic: `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` 
+* [PR #15551](https://github.com/leanprover-community/mathlib/pull/15551) set_theory/zfc/basic: `⊆` is reflexive, transitive, antisymmetric 
+* [PR #15549](https://github.com/leanprover-community/mathlib/pull/15549) set_theory/zfc/basic: add `refl`, `symm`, `trans` attributes to `equiv` lemmas 
+* [PR #15548](https://github.com/leanprover-community/mathlib/pull/15548) set_theory/zfc/ordinal: more lemmas on transitive sets 
+* [PR #15288](https://github.com/leanprover-community/mathlib/pull/15288) set_theory/zfc/ordinal: transitive sets 
+* [PR #15498](https://github.com/leanprover-community/mathlib/pull/15498) tactic/attribute: add `expand_exists` 
+* [PR #14762](https://github.com/leanprover-community/mathlib/pull/14762) tactic/compute_degree + test/compute_degree: introduce a tactic for proving `f.(nat_)degree ≤ d` 
+* [PR #14532](https://github.com/leanprover-community/mathlib/pull/14532) tactic/congrm: add "function underscores" to `congrm` 
+* [PR #15502](https://github.com/leanprover-community/mathlib/pull/15502) tactic/ext: don't remove attr 
+* [PR #15319](https://github.com/leanprover-community/mathlib/pull/15319) tactic/linear_combination: allow linear_combination to leave goal open 
+* [PR #15284](https://github.com/leanprover-community/mathlib/pull/15284) tactic/linear_combination: add parser for `h / a` 
+* [PR #15202](https://github.com/leanprover-community/mathlib/pull/15202) tactic/lint: add a linter for `[fintype _]` assumptions 
+* [PR #14878](https://github.com/leanprover-community/mathlib/pull/14878) tactic/polyrith: a tactic using Sage to solve polynomial equalities with hypotheses 
+* [PR #15618](https://github.com/leanprover-community/mathlib/pull/15618) tactic/positivity: a tactic for proving positivity/nonnegativity 
+* [PR #15728](https://github.com/leanprover-community/mathlib/pull/15728) test/polyrith: better formatting for generated tests 
+* [PR #15641](https://github.com/leanprover-community/mathlib/pull/15641) tooplogy/metric_space/hausdorff_distance: add lemmas about `thickening` 
+* [PR #15102](https://github.com/leanprover-community/mathlib/pull/15102) topology: basic simplification lemmas for `continuous_map`s 
+* [PR #14806](https://github.com/leanprover-community/mathlib/pull/14806) topology/algebra/filter_basis: add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group 
+* [PR #15157](https://github.com/leanprover-community/mathlib/pull/15157) topology/algebra/infinite_sum: Double sum is equal to a single value 
+* [PR #15610](https://github.com/leanprover-community/mathlib/pull/15610) topology/algebra/module/finite_dimension: add 2 simp lemmas 
+* [PR #15022](https://github.com/leanprover-community/mathlib/pull/15022) topology/algebra/order: ⁻¹ continuous for linear ordered fields 
+* [PR #14889](https://github.com/leanprover-community/mathlib/pull/14889) topology/algebra/uniform_group: `uniform_group` is preserved by Inf and comap 
+* [PR #15653](https://github.com/leanprover-community/mathlib/pull/15653) topology/basic: add lemmas about `filter.lift' _ closure` 
+* [PR #15580](https://github.com/leanprover-community/mathlib/pull/15580) topology/basic: a condition implying that a sequence of functions locally stabilizes 
+* [PR #15485](https://github.com/leanprover-community/mathlib/pull/15485) topology/basic: add 2 lemmas about `locally_finite` families 
+* [PR #14036](https://github.com/leanprover-community/mathlib/pull/14036) topology/continuous_function: Any T0 space embeds in a product of copies of the Sierpinski space 
+* [PR #14724](https://github.com/leanprover-community/mathlib/pull/14724) topology/homotopy: define nth homotopy group πₙ (without the group instance) 
+* [PR #15593](https://github.com/leanprover-community/mathlib/pull/15593) topology/instances/ennreal: add `continuous(_on).ennreal_mul` 
+* [PR #15446](https://github.com/leanprover-community/mathlib/pull/15446) topology/instances/nnreal: add `can_lift C(X, ℝ) C(X, ℝ≥0)` 
+* [PR #15311](https://github.com/leanprover-community/mathlib/pull/15311) topology/local_homeomorph: "injectivity" local_homeomorph.prod 
+* [PR #15612](https://github.com/leanprover-community/mathlib/pull/15612) topology/maps: add 2 lemmas, `open function` 
+* [PR #15165](https://github.com/leanprover-community/mathlib/pull/15165) topology/maps: more `iff` lemmas 
+* [PR #14926](https://github.com/leanprover-community/mathlib/pull/14926) topology/metric_space/hausdorff_distance: Thickening a compact inside an open 
+* [PR #15591](https://github.com/leanprover-community/mathlib/pull/15591) topology/metric_space/isometry: use namespace, add lemmas 
+* [PR #15634](https://github.com/leanprover-community/mathlib/pull/15634) topology/metric_space/lipschitz: add several lemmas 
+* [PR #14965](https://github.com/leanprover-community/mathlib/pull/14965) topology/noetherian_space: Noetherian spaces 
+* [PR #15617](https://github.com/leanprover-community/mathlib/pull/15617) topology/order: upgrade some lemmas to `iff`s 
+* [PR #15490](https://github.com/leanprover-community/mathlib/pull/15490) topology/partition_of_unity: local to global 
+* [PR #15635](https://github.com/leanprover-community/mathlib/pull/15635) topology/separation: add `disjoint_nhds_nhds` 
+* [PR #15043](https://github.com/leanprover-community/mathlib/pull/15043) topology/separation: `separation_quotient α` is a T₀ space 
+* [PR #15338](https://github.com/leanprover-community/mathlib/pull/15338) topology/sets/closeds: The coframe of closed sets 
+* [PR #15118](https://github.com/leanprover-community/mathlib/pull/15118) topology/sets/compacts: prod constructions 
+* [PR #15707](https://github.com/leanprover-community/mathlib/pull/15707) topology/subset_properties: `locally_compact_space` instance for `Π` types 
+* [PR #15484](https://github.com/leanprover-community/mathlib/pull/15484) topology/support: add lemmas, fix a name 
+* [PR #15346](https://github.com/leanprover-community/mathlib/pull/15346) topology/support: tsupport of product is a subset of tsupport 
+* [PR #14892](https://github.com/leanprover-community/mathlib/pull/14892) topology/uniform_space/basic: uniform continuity from/to an infimum of uniform spaces 

From 3e3ecf814ab79d20a4ab0e6c993b5a0f5bbfe693 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 3 Aug 2022 01:50:30 +0200
Subject: [PATCH 4/5] removed test

---
 posts/month-in-mathlib-jul-2022.md | 417 -----------------------------
 1 file changed, 417 deletions(-)
 delete mode 100644 posts/month-in-mathlib-jul-2022.md

diff --git a/posts/month-in-mathlib-jul-2022.md b/posts/month-in-mathlib-jul-2022.md
deleted file mode 100644
index fc66f416..00000000
--- a/posts/month-in-mathlib-jul-2022.md
+++ /dev/null
@@ -1,417 +0,0 @@
----
-author: 'Mathlib community'
-category: 'month-in-mathlib'
-date: 2022-08-03 00:49:41.091267
-description: ''
-has_math: true
-link: ''
-slug: month-in-mathlib-jul-2022
-tags: ''
-title: This month in mathlib (Jul 2022)
-type: text
----
-
-* [PR #15085](https://github.com/leanprover-community/mathlib/pull/15085) add lemmas about sigma types 
-* [PR #15609](https://github.com/leanprover-community/mathlib/pull/15609) /partition_of_unity: more lemmas based on the partition of unity 
-* [PR #15744](https://github.com/leanprover-community/mathlib/pull/15744) algebra/algebra/subalgebra/basic: Swap arguments of `map` and `comap` 
-* [PR #15556](https://github.com/leanprover-community/mathlib/pull/15556) algebra/big_operators: add lemmas about sum of disjoint multiset 
-* [PR #15095](https://github.com/leanprover-community/mathlib/pull/15095) algebra/category: forgetful functors from modules reflect limits 
-* [PR #15019](https://github.com/leanprover-community/mathlib/pull/15019) algebra/category/BoolRing: The equivalence between Boolean rings and Boolean algebras 
-* [PR #15330](https://github.com/leanprover-community/mathlib/pull/15330) algebra/category/Group: The forgetful-units adjunction between `Group` and `Mon`. 
-* [PR #14328](https://github.com/leanprover-community/mathlib/pull/14328) algebra/category/Module: upgrade `free : Type ⥤ Module R` to a monoidal functor 
-* [PR #14720](https://github.com/leanprover-community/mathlib/pull/14720) algebra/category_theory/Group/epi_mono: about monomorphism and epimorphism in category of group 
-* [PR #15654](https://github.com/leanprover-community/mathlib/pull/15654) algebra/direct_sum/decomposition: add an induction principle for `direct_sum.decomposition` class 
-* [PR #15109](https://github.com/leanprover-community/mathlib/pull/15109) algebra/gcd_monoid: GCD domains are integrally closed. 
-* [PR #15403](https://github.com/leanprover-community/mathlib/pull/15403) algebra/group/with_one: units of a group with zero is isomorphic to the group 
-* [PR #14945](https://github.com/leanprover-community/mathlib/pull/14945) algebra/homology: homotopy equivalences are quasi-isomorphisms 
-* [PR #11073](https://github.com/leanprover-community/mathlib/pull/11073) algebra/jordan: Introduce Jordan rings 
-* [PR #14179](https://github.com/leanprover-community/mathlib/pull/14179) algebra/lie/cartan_subalgebra: characterise Cartan subalgebras as limiting values of upper central series 
-* [PR #15675](https://github.com/leanprover-community/mathlib/pull/15675) algebra/lie/of_associative: add `commute.lie_eq` 
-* [PR #15733](https://github.com/leanprover-community/mathlib/pull/15733) algebra/module: sub_mem_sup for modules over rings 
-* [PR #12895](https://github.com/leanprover-community/mathlib/pull/12895) algebra/module: add injective module and Baer's criterion 
-* [PR #15103](https://github.com/leanprover-community/mathlib/pull/15103) algebra/module/linear_map: use morphisms class for lemmas about linear [pre]images of `c • S` 
-* [PR #14470](https://github.com/leanprover-community/mathlib/pull/14470) algebra/module/localized_module: construction of module localisation 
-* [PR #15092](https://github.com/leanprover-community/mathlib/pull/15092) algebra/module/torsion: `R/I`-module structure on `M/IM`. 
-* [PR #3292](https://github.com/leanprover-community/mathlib/pull/3292) algebra/order/complete_field: `conditionally_complete_linear_ordered_field`, aka the reals 
-* [PR #15300](https://github.com/leanprover-community/mathlib/pull/15300) algebra/order/monoid: add lemmas `map_add` for `with_bot/top` 
-* [PR #15458](https://github.com/leanprover-community/mathlib/pull/15458) algebra/order/monoid: add `one_lt_mul_iff`/`add_pos_iff` 
-* [PR #15219](https://github.com/leanprover-community/mathlib/pull/15219) algebra/order/monoid: Add zero_le_three and zero_le_four 
-* [PR #15267](https://github.com/leanprover-community/mathlib/pull/15267) algebra/order/monoid_lemmas: add `antitone`, `monotone_on`, and `antitone_on` lemmas 
-* [PR #14761](https://github.com/leanprover-community/mathlib/pull/14761) algebra/order/monoid_lemmas_zero_lt: add some lemmas about typeclasses 
-* [PR #14770](https://github.com/leanprover-community/mathlib/pull/14770) algebra/order/monoid_lemmas_zero_lt: add missing lemmas 
-* [PR #15186](https://github.com/leanprover-community/mathlib/pull/15186) algebra/parity: more general odd.pos 
-* [PR #15660](https://github.com/leanprover-community/mathlib/pull/15660) algebra/periodic: `fract_periodic` 
-* [PR #13958](https://github.com/leanprover-community/mathlib/pull/13958) algebra/ring/{pi, prod, opposite}: add basic defs for non_unital_ring_hom 
-* [PR #15291](https://github.com/leanprover-community/mathlib/pull/15291) algebraic_geometry: comap of surjective homomorphism is closed embedding 
-* [PR #11649](https://github.com/leanprover-community/mathlib/pull/11649) algebraic_geometry: Intersection of affine open can be covered by common basic opens 
-* [PR #14972](https://github.com/leanprover-community/mathlib/pull/14972) algebraic_geometry: Restriction of morphisms onto open sets of the target 
-* [PR #15487](https://github.com/leanprover-community/mathlib/pull/15487) algebraic_geometry/AffineScheme: Affine communication lemma 
-* [PR #15365](https://github.com/leanprover-community/mathlib/pull/15365) algebraic_geometry/EllipticCurve: simplify definition of discriminant 
-* [PR #15436](https://github.com/leanprover-community/mathlib/pull/15436) algebraic_geometry/morphisms: Quasi-compact morphisms of schemes 
-* [PR #14944](https://github.com/leanprover-community/mathlib/pull/14944) algebraic_geometry/morphisms: Basic framework for classes of morphisms between schemes 
-* [PR #13397](https://github.com/leanprover-community/mathlib/pull/13397) algebraic_geometry/projective_spectrum: forward direction of homeomorphism between top_space of Proj and top_space of Spec 
-* [PR #14588](https://github.com/leanprover-community/mathlib/pull/14588) algebraic_topology: alternating_coface_map_complex 
-* [PR #15616](https://github.com/leanprover-community/mathlib/pull/15616) algebraic_topology/dold_kan: construction of idempotent endomorphisms 
-* [PR #14044](https://github.com/leanprover-community/mathlib/pull/14044) algebraic_topology/dold_kan: technical lemmas about face maps 
-* [PR #12788](https://github.com/leanprover-community/mathlib/pull/12788) algebraic_topology/fundamental_groupoid: Define simply connected spaces 
-* [PR #15568](https://github.com/leanprover-community/mathlib/pull/15568) analysis/asymptotics: add `is_o*.of_pow` 
-* [PR #15010](https://github.com/leanprover-community/mathlib/pull/15010) analysis/asymptotics/asymptotics: generalize, golf 
-* [PR #15416](https://github.com/leanprover-community/mathlib/pull/15416) analysis/calculus: generalize `differentiable*.pow`, add `differentiable*.zpow` 
-* [PR #15595](https://github.com/leanprover-community/mathlib/pull/15595) analysis/calculus/cont_diff: generalize `mul` lemmas to a normed algebra 
-* [PR #15309](https://github.com/leanprover-community/mathlib/pull/15309) analysis/calculus/cont_diff: extra lemmas about cont_diff_within_at 
-* [PR #15133](https://github.com/leanprover-community/mathlib/pull/15133) analysis/calculus/mean_value: remove assumption in strict_mono_on.strict_convex_on_of_deriv 
-* [PR #15122](https://github.com/leanprover-community/mathlib/pull/15122) analysis/complex: equiv_real_prod_symm_apply 
-* [PR #15364](https://github.com/leanprover-community/mathlib/pull/15364) analysis/complex/abs_max: add a version of the maximum modulus principle 
-* [PR #15639](https://github.com/leanprover-community/mathlib/pull/15639) analysis/convex/cone: add inner_dual_cone_eq_Inter_inner_dual_cone_singleton 
-* [PR #14821](https://github.com/leanprover-community/mathlib/pull/14821) analysis/convex/function: Variants of `convex_on.le_right_of_left_le` 
-* [PR #15363](https://github.com/leanprover-community/mathlib/pull/15363) analysis/inner_product/calculus: [higher] differentiability to/from `euclidean_space` 
-* [PR #15481](https://github.com/leanprover-community/mathlib/pull/15481) analysis/inner_product/pi_L2: a finite orthonormal family is a basis of its span 
-* [PR #15540](https://github.com/leanprover-community/mathlib/pull/15540) analysis/inner_product_space: in finite dimension, hilbert basis = orthonormal basis 
-* [PR #15055](https://github.com/leanprover-community/mathlib/pull/15055) analysis/inner_product_space: the Hellinger-Toeplitz theorem 
-* [PR #15020](https://github.com/leanprover-community/mathlib/pull/15020) analysis/inner_product_space: add simple lemmas for the orthogonal complement 
-* [PR #15514](https://github.com/leanprover-community/mathlib/pull/15514) analysis/inner_product_space/[pi_L2, l2_space]: compute inner product in a given [orthonormal, hilbert] basis 
-* [PR #15577](https://github.com/leanprover-community/mathlib/pull/15577) analysis/inner_product_space/basic: `orthonormal` version of `linear_independent.coe_range` 
-* [PR #15470](https://github.com/leanprover-community/mathlib/pull/15470) analysis/inner_product_space/positive: definition and basic facts about positive operators 
-* [PR #14876](https://github.com/leanprover-community/mathlib/pull/14876) analysis/locally_convex/basic: a few lemmas about balanced sets 
-* [PR #15124](https://github.com/leanprover-community/mathlib/pull/15124) analysis/locally_convex/with_seminorms: in a normed space, von Neumann bounded = metric bounded 
-* [PR #15515](https://github.com/leanprover-community/mathlib/pull/15515) analysis/normed: add instances and lemmas 
-* [PR #15467](https://github.com/leanprover-community/mathlib/pull/15467) analysis/normed_space/compact_operator: definition and basic facts about compact operators 
-* [PR #15650](https://github.com/leanprover-community/mathlib/pull/15650) analysis/normed_space/linear_isometry: add defs and lemmas 
-* [PR #15471](https://github.com/leanprover-community/mathlib/pull/15471) analysis/normed_space/linear_isometry: `linear_equiv.of_eq` as a `linear_isometry_equiv` 
-* [PR #15317](https://github.com/leanprover-community/mathlib/pull/15317) analysis/normed_space/lp_space: construct star structures on lp spaces 
-* [PR #15086](https://github.com/leanprover-community/mathlib/pull/15086) analysis/normed_space/lp_space: normed_algebra structure 
-* [PR #14104](https://github.com/leanprover-community/mathlib/pull/14104) analysis/normed_space/lp_space: add l_infinity ring instances 
-* [PR #15578](https://github.com/leanprover-community/mathlib/pull/15578) analysis/normed_space/operator_norm: variant of `continuous_linear_equiv.has_sum` 
-* [PR #15417](https://github.com/leanprover-community/mathlib/pull/15417) analysis/normed_space/operator_norm: add 2 new versions of `op_norm_le_*` 
-* [PR #15173](https://github.com/leanprover-community/mathlib/pull/15173) analysis/normed_space/star/basic: make starₗᵢ apply to normed star groups 
-* [PR #15125](https://github.com/leanprover-community/mathlib/pull/15125) analysis/special_functions/complex/arg: add complex.abs_eq_one_iff 
-* [PR #14980](https://github.com/leanprover-community/mathlib/pull/14980) analysis/special_functions/complex/arg: `continuous_at_arg_coe_angle` 
-* [PR #15506](https://github.com/leanprover-community/mathlib/pull/15506) analysis/special_functions/exp: add lemmas about `is_o`/`is_O`/`is_Theta` 
-* [PR #15106](https://github.com/leanprover-community/mathlib/pull/15106) analysis/special_functions/gaussian: formula for gaussian integrals 
-* [PR #15258](https://github.com/leanprover-community/mathlib/pull/15258) analysis/special_functions/polar_coord: define polar coordinates, polar change of variable formula in integrals 
-* [PR #15164](https://github.com/leanprover-community/mathlib/pull/15164) analysis/special_functions/pow: drop an assumption in `is_o_log_rpow_rpow_at_top` 
-* [PR #15002](https://github.com/leanprover-community/mathlib/pull/15002) analysis/special_functions/pow: Rational powers are dense 
-* [PR #15651](https://github.com/leanprover-community/mathlib/pull/15651) analysis/special_functions/trigonometric/angle: equality of `cos` or `sin` 
-* [PR #14988](https://github.com/leanprover-community/mathlib/pull/14988) analysis/special_functions/trigonometric/angle: equality of twice angles 
-* [PR #15360](https://github.com/leanprover-community/mathlib/pull/15360) big_operators/fin: sum over elements of vector equal to `a` equals count `a` 
-* [PR #14422](https://github.com/leanprover-community/mathlib/pull/14422) category_theory: construction of the localized category 
-* [PR #14838](https://github.com/leanprover-community/mathlib/pull/14838) category_theory: a characterization of separating objects 
-* [PR #14974](https://github.com/leanprover-community/mathlib/pull/14974) category_theory: full_of_surjective 
-* [PR #15238](https://github.com/leanprover-community/mathlib/pull/15238) category_theory: a category with a small detecting set is well-powered 
-* [PR #15377](https://github.com/leanprover-community/mathlib/pull/15377) category_theory: limits of essentially small indexing categories 
-* [PR #14880](https://github.com/leanprover-community/mathlib/pull/14880) category_theory: (co)products and (co)separators 
-* [PR #14026](https://github.com/leanprover-community/mathlib/pull/14026) category_theory: left-exact functors preserve finite limits 
-* [PR #15121](https://github.com/leanprover-community/mathlib/pull/15121) category_theory//algebra: epi_of_epi and mono_of_mono 
-* [PR #14581](https://github.com/leanprover-community/mathlib/pull/14581) category_theory/abelian/: functors that preserve finite limits and colimits preserve exactness 
-* [PR #14834](https://github.com/leanprover-community/mathlib/pull/14834) category_theory/endofunctor/algebra: Define coalgebras over an endofunctor and prove an equivalence 
-* [PR #14829](https://github.com/leanprover-community/mathlib/pull/14829) category_theory/functor: preserving/reflecting monos/epis 
-* [PR #14419](https://github.com/leanprover-community/mathlib/pull/14419) category_theory/limits: preserves biproducts if comparison is iso 
-* [PR #14526](https://github.com/leanprover-community/mathlib/pull/14526) category_theory/limits: opposites of limit pullback cones 
-* [PR #14452](https://github.com/leanprover-community/mathlib/pull/14452) category_theory/limits: bilimit from kernel 
-* [PR #14948](https://github.com/leanprover-community/mathlib/pull/14948) category_theory/limits/construction: Construct finite limits from terminal objects and pullbacks 
-* [PR #15269](https://github.com/leanprover-community/mathlib/pull/15269) category_theory/limits/shapes/comm_sq: opposites of is_pullback and is_pushout 
-* [PR #14445](https://github.com/leanprover-community/mathlib/pull/14445) category_theory/preadditive: constructing a semiadditive structure from binary biproducts 
-* [PR #15096](https://github.com/leanprover-community/mathlib/pull/15096) category_theory/preadditive: left exactness of certain hom functors 
-* [PR #14832](https://github.com/leanprover-community/mathlib/pull/14832) category_theory/preadditive: projective iff coyoneda.obj preserves epimorphisms 
-* [PR #15100](https://github.com/leanprover-community/mathlib/pull/15100) category_theory/preadditive: algebra over endofunctor preadditive and forget additive functor 
-* [PR #15455](https://github.com/leanprover-community/mathlib/pull/15455) category_theory/shapes/pullbacks: Pullbacks isomorphic to the opposite of pushouts 
-* [PR #14831](https://github.com/leanprover-community/mathlib/pull/14831) category_theory/yoneda: coyoneda.obj_op_op 
-* [PR #15327](https://github.com/leanprover-community/mathlib/pull/15327) combinatorics/additive/behrend: Behrend's lower bound on Roth numbers 
-* [PR #14070](https://github.com/leanprover-community/mathlib/pull/14070) combinatorics/additive/behrend: Behrend's construction 
-* [PR #14697](https://github.com/leanprover-community/mathlib/pull/14697) combinatorics/additive/ruzsa_covering: The Ruzsa covering lemma 
-* [PR #14497](https://github.com/leanprover-community/mathlib/pull/14497) combinatorics/set_family/harris_kleitman: The Harris-Kleitman inequality 
-* [PR #14475](https://github.com/leanprover-community/mathlib/pull/14475) combinatorics/set_family/intersecting: Intersecting families 
-* [PR #14543](https://github.com/leanprover-community/mathlib/pull/14543) combinatorics/set_family/kleitman: Kleitman's bound 
-* [PR #15150](https://github.com/leanprover-community/mathlib/pull/15150) combinatorics/simple_graph/basic: `dart.to_prod` is injective 
-* [PR #15156](https://github.com/leanprover-community/mathlib/pull/15156) combinatorics/simple_graph/connectivity: operations and lemmas about path type 
-* [PR #15153](https://github.com/leanprover-community/mathlib/pull/15153) combinatorics/simple_graph/connectivity: simp confluence 
-* [PR #15353](https://github.com/leanprover-community/mathlib/pull/15353) combinatorics/simple_graph/density: Bound on the difference between edge densities 
-* [PR #14978](https://github.com/leanprover-community/mathlib/pull/14978) combinatorics/simple_graph/hasse: The Hasse diagram of `α × β` 
-* [PR #14867](https://github.com/leanprover-community/mathlib/pull/14867) combinatorics/simple_graph/prod: Box product 
-* [PR #13222](https://github.com/leanprover-community/mathlib/pull/13222) combinatorics/simple_graph/regularity/equitabilise: Equitabilising a partition 
-* [PR #14403](https://github.com/leanprover-community/mathlib/pull/14403) combinatorics/simple_graph/subgraph: delete vertices in a subgraph 
-* [PR #14877](https://github.com/leanprover-community/mathlib/pull/14877) combinatorics/simple_graph/subgraph: add `subgraph.comap` and subgraph of subgraph coercion 
-* [PR #15158](https://github.com/leanprover-community/mathlib/pull/15158) combinatorics/simple_graph/trails: Euler's condition for trails  
-* [PR #14034](https://github.com/leanprover-community/mathlib/pull/14034) combinatorics/simple_graph/{basic,subgraph,clique,coloring}: add induced graphs, characterization of cliques, and bounds for colorings 
-* [PR #15505](https://github.com/leanprover-community/mathlib/pull/15505) computability/ackermann: the Ackermann function isn't primitive recursive 
-* [PR #15280](https://github.com/leanprover-community/mathlib/pull/15280) data/countable: add `countable` typeclass 
-* [PR #15337](https://github.com/leanprover-community/mathlib/pull/15337) data/fin/basic: add a reflected instance 
-* [PR #15048](https://github.com/leanprover-community/mathlib/pull/15048) data/fin/tuple/basic: add lemmas for rewriting exists and forall over `n+1`-tuples 
-* [PR #15607](https://github.com/leanprover-community/mathlib/pull/15607) data/finset/basic: There is exactly one set in empty types 
-* [PR #15385](https://github.com/leanprover-community/mathlib/pull/15385) data/finset/basic: lemmas about `filter`, `cons`, and `disj_union` 
-* [PR #15170](https://github.com/leanprover-community/mathlib/pull/15170) data/finset/basic: Add `decidable_nonempty` for finsets. 
-* [PR #15011](https://github.com/leanprover-community/mathlib/pull/15011) data/finset/basic: Coercion of a product of finsets 
-* [PR #15257](https://github.com/leanprover-community/mathlib/pull/15257) data/finset/fold: add lemma `fold_max_add` 
-* [PR #15212](https://github.com/leanprover-community/mathlib/pull/15212) data/finset/lattice: add three.2 lemmas about `finset.max/min` 
-* [PR #15435](https://github.com/leanprover-community/mathlib/pull/15435) data/finset/pointwise: Singleton arithmetic 
-* [PR #15387](https://github.com/leanprover-community/mathlib/pull/15387) data/finset/powerset: More `powerset` lemmas 
-* [PR #15197](https://github.com/leanprover-community/mathlib/pull/15197) data/finsupp/basic: graph of a finitely supported function 
-* [PR #15155](https://github.com/leanprover-community/mathlib/pull/15155) data/finsupp/big_operators: sum of finsupp and their support 
-* [PR #15080](https://github.com/leanprover-community/mathlib/pull/15080) data/fintype/basic: add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. 
-* [PR #15207](https://github.com/leanprover-community/mathlib/pull/15207) data/json: helper functions for json serialization 
-* [PR #15138](https://github.com/leanprover-community/mathlib/pull/15138) data/list: accessing list with fallback 
-* [PR #15472](https://github.com/leanprover-community/mathlib/pull/15472) data/list/basic: when drop_while and take_while hold 
-* [PR #15482](https://github.com/leanprover-community/mathlib/pull/15482) data/list/basic: last_reverse 
-* [PR #15139](https://github.com/leanprover-community/mathlib/pull/15139) data/list/basic: nth_le_enum 
-* [PR #14777](https://github.com/leanprover-community/mathlib/pull/14777) data/list/basic: add filter_map_join 
-* [PR #15473](https://github.com/leanprover-community/mathlib/pull/15473) data/list/infix: drop_while and take_while suf/prefix 
-* [PR #15433](https://github.com/leanprover-community/mathlib/pull/15433) data/list/of_fn: lemmas to turn quantifiers over lists to quantifiers over tuples 
-* [PR #15386](https://github.com/leanprover-community/mathlib/pull/15386) data/matrix/basic: Add `alg_equiv` and `linear_equiv` instances for transpose. 
-* [PR #14991](https://github.com/leanprover-community/mathlib/pull/14991) data/matrix/notation: add `!![1, 2; 3, 4]` notation 
-* [PR #15094](https://github.com/leanprover-community/mathlib/pull/15094) data/multiset/fintype: coercion from multiset to type 
-* [PR #15457](https://github.com/leanprover-community/mathlib/pull/15457) data/nat/basic: add recursion principle `even_odd_rec` as a wrapper around `binary_rec` 
-* [PR #15061](https://github.com/leanprover-community/mathlib/pull/15061) data/nat/basic: add `strong_sub_recursion` and `pincer_recursion` 
-* [PR #15099](https://github.com/leanprover-community/mathlib/pull/15099) data/nat/basic: split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas 
-* [PR #15031](https://github.com/leanprover-community/mathlib/pull/15031) data/nat/basic: add `mul_div_mul_comm_of_dvd_dvd` 
-* [PR #15409](https://github.com/leanprover-community/mathlib/pull/15409) data/nat/bitwise: tweak `lxor` lemmas 
-* [PR #15072](https://github.com/leanprover-community/mathlib/pull/15072) data/nat/choose/basic: Definition of `multichoose` and basic lemmas 
-* [PR #15029](https://github.com/leanprover-community/mathlib/pull/15029) data/nat/enat: simple lemmas on `enat` 
-* [PR #15767](https://github.com/leanprover-community/mathlib/pull/15767) data/nat/factorization/basic: add lemma `prime.factorization_self` 
-* [PR #15277](https://github.com/leanprover-community/mathlib/pull/15277) data/nat/factorization/basic: golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` 
-* [PR #15014](https://github.com/leanprover-community/mathlib/pull/15014) data/nat/factorization/basic: add lemma `factorization_eq_card_pow_dvd` 
-* [PR #15539](https://github.com/leanprover-community/mathlib/pull/15539) data/nat/pairing: basic bounds on `mkpair` 
-* [PR #15268](https://github.com/leanprover-community/mathlib/pull/15268) data/nat/parity: `nat.bit1_div_bit0` 
-* [PR #15645](https://github.com/leanprover-community/mathlib/pull/15645) data/nat/totient: lemmas `totient_mul_of_prime_of_{not_}dvd` 
-* [PR #15313](https://github.com/leanprover-community/mathlib/pull/15313) data/pfun: tooling to help reasoning about pfun domains 
-* [PR #15588](https://github.com/leanprover-community/mathlib/pull/15588) data/pi/algebra: sum_elim lemmas 
-* [PR #15508](https://github.com/leanprover-community/mathlib/pull/15508) data/pnat/basic: add lemmas, move `equiv.pnat_equiv_nat` 
-* [PR #15183](https://github.com/leanprover-community/mathlib/pull/15183) data/pnat/basic: `succ` as an order isomorphism between `ℕ` and `ℕ+` 
-* [PR #15199](https://github.com/leanprover-community/mathlib/pull/15199) data/polynomial/degree/definitions: redefine `polynomial.degree` as `p.support.max` 
-* [PR #15522](https://github.com/leanprover-community/mathlib/pull/15522) data/polynomial/degree/lemmas: three lemmas on nat_degrees, bits and neg 
-* [PR #14741](https://github.com/leanprover-community/mathlib/pull/14741) data/polynomial/erase_lead: Characterization of polynomials of fixed support 
-* [PR #15225](https://github.com/leanprover-community/mathlib/pull/15225) data/polynomial/laurent: define `degree` and some API 
-* [PR #15318](https://github.com/leanprover-community/mathlib/pull/15318) data/polynomial/unit_trinomial: Irreducibility of X^n-X-1 
-* [PR #14914](https://github.com/leanprover-community/mathlib/pull/14914) data/polynomial/unit_trinomial: An irreducibility criterion for unit trinomials 
-* [PR #15148](https://github.com/leanprover-community/mathlib/pull/15148) data/quot: `is_equiv` instance for quotient equivalence 
-* [PR #15101](https://github.com/leanprover-community/mathlib/pull/15101) data/rat/defs: add denominator as pnat 
-* [PR #15575](https://github.com/leanprover-community/mathlib/pull/15575) data/real/basic: add a repr showing an underlying cauchy sequence 
-* [PR #15483](https://github.com/leanprover-community/mathlib/pull/15483) data/real/{e,}nnreal: images and preimages of `ord_connected` sets 
-* [PR #14970](https://github.com/leanprover-community/mathlib/pull/14970) data/set/basic,order/filter/basic: add semiconj lemmas about images and maps 
-* [PR #15671](https://github.com/leanprover-community/mathlib/pull/15671) data/set/countable: add `iff` versions of some lemmas 
-* [PR #15415](https://github.com/leanprover-community/mathlib/pull/15415) data/set/countable: protect lemmas 
-* [PR #15444](https://github.com/leanprover-community/mathlib/pull/15444) data/set/finite: set.finite.induction_on' 
-* [PR #15177](https://github.com/leanprover-community/mathlib/pull/15177) data/set/finite: add `multiset.finite_to_set` 
-* [PR #15605](https://github.com/leanprover-community/mathlib/pull/15605) data/set/function: add lemmas about `set.restrict` 
-* [PR #15608](https://github.com/leanprover-community/mathlib/pull/15608) data/set/intervals: add lemmas 
-* [PR #14928](https://github.com/leanprover-community/mathlib/pull/14928) data/set/pointwise: `list` and `multiset` versions of n-ary lemmas 
-* [PR #15604](https://github.com/leanprover-community/mathlib/pull/15604) data/set/prod: add theorems about `λ x, (x, x)` 
-* [PR #15652](https://github.com/leanprover-community/mathlib/pull/15652) data/sign: `left.sign_neg`, `right.sign_neg` 
-* [PR #15358](https://github.com/leanprover-community/mathlib/pull/15358) data/sum/basic: `sum.lift_rel` is a subrelation of `sum.lex` 
-* [PR #15370](https://github.com/leanprover-community/mathlib/pull/15370) data/sum/order: `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` 
-* [PR #15192](https://github.com/leanprover-community/mathlib/pull/15192) data/sym/basic: combinatorial equivalence for `sym (option α) n.succ` 
-* [PR #11162](https://github.com/leanprover-community/mathlib/pull/11162) data/sym/card: Prove stars and bars 
-* [PR #15383](https://github.com/leanprover-community/mathlib/pull/15383) data/vector/basic: make the recursor work with `induction _ using` syntax 
-* [PR #15154](https://github.com/leanprover-community/mathlib/pull/15154) data/vector/mem: Lemmas about membership in a vector 
-* [PR #15493](https://github.com/leanprover-community/mathlib/pull/15493) data/{finset,set}/basic: `insert a s = s ↔ a ∈ s` 
-* [PR #15478](https://github.com/leanprover-community/mathlib/pull/15478) data/{pi, prod}: add missing `has_pow` instances for `pi` type 
-* [PR #15724](https://github.com/leanprover-community/mathlib/pull/15724) field_theory/adjoin: A compositum of algebraic extensions is algebraic 
-* [PR #15426](https://github.com/leanprover-community/mathlib/pull/15426) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version 
-* [PR #15518](https://github.com/leanprover-community/mathlib/pull/15518) field_theory/adjoin: `intermediate_field.exists_finset_of_mem_supr` 
-* [PR #15438](https://github.com/leanprover-community/mathlib/pull/15438) field_theory/adjoin: Compact elements of `intermediate_field` 
-* [PR #15420](https://github.com/leanprover-community/mathlib/pull/15420) field_theory/adjoin: `F⟮α⟯ ≤ K ↔ α ∈ K` 
-* [PR #15339](https://github.com/leanprover-community/mathlib/pull/15339) field_theory/adjoin: The compositum of finitely many finite dimensional intermediate fields is finite dimensional 
-* [PR #15659](https://github.com/leanprover-community/mathlib/pull/15659) field_theory/intermediate_field: Produce an intermediate field from a subalgebra satisfying `is_field`. 
-* [PR #15188](https://github.com/leanprover-community/mathlib/pull/15188) field_theory/intermediate_field: `dsimp` lemma 
-* [PR #15303](https://github.com/leanprover-community/mathlib/pull/15303) field_theory/tower: if `L / K / F` is finite, so is `K / F` 
-* [PR #15021](https://github.com/leanprover-community/mathlib/pull/15021) geometry/euclidean/basic: `continuous_at_angle` 
-* [PR #15463](https://github.com/leanprover-community/mathlib/pull/15463) geometry/euclidean/oriented_angle: `continuous_at_oangle` 
-* [PR #15560](https://github.com/leanprover-community/mathlib/pull/15560) geometry/manifold: generalize some lemmas from `smooth` to `cont_mdiff` 
-* [PR #15116](https://github.com/leanprover-community/mathlib/pull/15116) geometry/manifold/local_invariant_properties: simplify definitions and proofs 
-* [PR #15437](https://github.com/leanprover-community/mathlib/pull/15437) geometry/manifold/metrizable: metrizability of a manifold 
-* [PR #15314](https://github.com/leanprover-community/mathlib/pull/15314) geometry/manifold|topology: add simps and ext attributes 
-* [PR #14182](https://github.com/leanprover-community/mathlib/pull/14182) group_theory/complement: transversal for the transfer homomorphism 
-* [PR #15402](https://github.com/leanprover-community/mathlib/pull/15402) group_theory/finite_abelian: a finitely generated torsion abelian group is finite 
-* [PR #15239](https://github.com/leanprover-community/mathlib/pull/15239) group_theory/group_action/option: Scalar action on an option 
-* [PR #15050](https://github.com/leanprover-community/mathlib/pull/15050) group_theory/group_action/sub_mul_action: add the pointwise monoid structure 
-* [PR #8632](https://github.com/leanprover-community/mathlib/pull/8632) group_theory/p_group: Groups of order p^2 are commutative 
-* [PR #15052](https://github.com/leanprover-community/mathlib/pull/15052) group_theory/submonoid/pointwise: add the pointwise monoid structure on `add_submonoid` 
-* [PR #13945](https://github.com/leanprover-community/mathlib/pull/13945) group_theory/subsemigroup/membership: add membership criteria for subsemigroups 
-* [PR #14739](https://github.com/leanprover-community/mathlib/pull/14739) information_theory/hamming: add Hamming distance and norm 
-* [PR #15603](https://github.com/leanprover-community/mathlib/pull/15603) integration: elementary version of FTC-1 
-* [PR #15587](https://github.com/leanprover-community/mathlib/pull/15587) linear_algebra: lemmas on associatedness of determinants of linear maps 
-* [PR #15119](https://github.com/leanprover-community/mathlib/pull/15119) linear_algebra: basis on R × R, and relation between matrices and linear maps in this basis  
-* [PR #14714](https://github.com/leanprover-community/mathlib/pull/14714) linear_algebra: add lemma `linear_independent.finite_of_is_noetherian` 
-* [PR #12140](https://github.com/leanprover-community/mathlib/pull/12140) linear_algebra/annihilating_polynomial: add definition of annihilating ideal and show minpoly generates in field case 
-* [PR #14883](https://github.com/leanprover-community/mathlib/pull/14883) linear_algebra/basis: shows the lattice of submodules of a module over a division ring is atomistic 
-* [PR #14790](https://github.com/leanprover-community/mathlib/pull/14790) linear_algebra/clifford_algebra/even: Universal property and isomorphisms for the even subalgebra 
-* [PR #15558](https://github.com/leanprover-community/mathlib/pull/15558) linear_algebra/finite_dimensional: One-dimensional iff principal 
-* [PR #15531](https://github.com/leanprover-community/mathlib/pull/15531) linear_algebra/linear_pmap: more lemmas about the graph 
-* [PR #14922](https://github.com/leanprover-community/mathlib/pull/14922) linear_algebra/linear_pmap: construct a `linear_pmap` from its graph 
-* [PR #14794](https://github.com/leanprover-community/mathlib/pull/14794) linear_algebra/matrix: inner prod of matrix 
-* [PR #15459](https://github.com/leanprover-community/mathlib/pull/15459) linear_algebra/matrix/charpoly: Coefficients of the characteristic polynomial falls in the ideal power. 
-* [PR #15391](https://github.com/leanprover-community/mathlib/pull/15391) linear_algebra/projective_space/subspace: defines subspaces of a projective space 
-* [PR #14542](https://github.com/leanprover-community/mathlib/pull/14542) linear_algebra/projectivization/independence: defines (in)dependence of points in projective space 
-* [PR #15628](https://github.com/leanprover-community/mathlib/pull/15628) linear_algebra/tensor_product: add id_apply and comp_apply for ltensor and rtensor 
-* [PR #15209](https://github.com/leanprover-community/mathlib/pull/15209) linear_algebra/unitary_group: better constructor 
-* [PR #15524](https://github.com/leanprover-community/mathlib/pull/15524) logic/encodable/basic: an encodable type is countable 
-* [PR #15611](https://github.com/leanprover-community/mathlib/pull/15611) logic/equiv/local_equiv: add 2 lemmas 
-* [PR #15176](https://github.com/leanprover-community/mathlib/pull/15176) logic/equiv/set: define `equiv.set.pi` 
-* [PR #15574](https://github.com/leanprover-community/mathlib/pull/15574) logic/nonempty: `pi.nonempty` instance 
-* [PR #15307](https://github.com/leanprover-community/mathlib/pull/15307) measure_theory/constructions/borel_space: the set of points for which a measurable sequence of functions converges is measurable 
-* [PR #14424](https://github.com/leanprover-community/mathlib/pull/14424) measure_theory/constructions/prod: The layercake integral. 
-* [PR #15422](https://github.com/leanprover-community/mathlib/pull/15422) measure_theory/function/conditional_expecation: conditional expectation of a function to a independent sigma-algebra  
-* [PR #15274](https://github.com/leanprover-community/mathlib/pull/15274) measure_theory/function/conditional_expectation: pull-out property of the conditional expectation 
-* [PR #15024](https://github.com/leanprover-community/mathlib/pull/15024) measure_theory/function/conditional_expectation: monotonicity of the conditional expectation 
-* [PR #15378](https://github.com/leanprover-community/mathlib/pull/15378) measure_theory/function/uniform_integrable: conditional expectations form a uniformly integrable class 
-* [PR #15120](https://github.com/leanprover-community/mathlib/pull/15120) measure_theory/group/measure: a product of Haar measures is a Haar measure 
-* [PR #15423](https://github.com/leanprover-community/mathlib/pull/15423) measure_theory/integral: generalize some integral properties to set_to_fun 
-* [PR #13885](https://github.com/leanprover-community/mathlib/pull/13885) measure_theory/integral: Circle integral transform 
-* [PR #15344](https://github.com/leanprover-community/mathlib/pull/15344) measure_theory/integral/set_integral: add `set_integral_indicator` 
-* [PR #15342](https://github.com/leanprover-community/mathlib/pull/15342) measure_theory/measurable_space_def: add `generate_from_induction` 
-* [PR #15528](https://github.com/leanprover-community/mathlib/pull/15528) measure_theory/measure/finite_measure_weak_convergence: Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. 
-* [PR #15205](https://github.com/leanprover-community/mathlib/pull/15205) measure_theory/measure/finite_measure_weak_convergence: Add some missing API lemmas. 
-* [PR #15343](https://github.com/leanprover-community/mathlib/pull/15343) measure_theory/measure/measure_space: generalize measure.comap 
-* [PR #15066](https://github.com/leanprover-community/mathlib/pull/15066) measure_theory/pmf: lawful monad instance for probability mass function monad 
-* [PR #8002](https://github.com/leanprover-community/mathlib/pull/8002) number_theory: Bertrand's postulate, slightly different approach 
-* [PR #15315](https://github.com/leanprover-community/mathlib/pull/15315) number_theory: degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` 
-* [PR #15418](https://github.com/leanprover-community/mathlib/pull/15418) number_theory/legendre_symbol/: redefine quadratic characters as `mul_char`s 
-* [PR #15499](https://github.com/leanprover-community/mathlib/pull/15499) number_theory/legendre_symbol/add_character: add file introducing additive characters 
-* [PR #15007](https://github.com/leanprover-community/mathlib/pull/15007) number_theory/slash_actions: Slash actions class for modular forms 
-* [PR #14717](https://github.com/leanprover-community/mathlib/pull/14717) number_theory/wilson: add Wilson's Theorem 
-* [PR #15149](https://github.com/leanprover-community/mathlib/pull/15149) order/basic: a symmetric relation implies equality when it implies less-equal 
-* [PR #15606](https://github.com/leanprover-community/mathlib/pull/15606) order/boolean_algebra: A bounded generalized boolean algebra is a boolean algebra 
-* [PR #15278](https://github.com/leanprover-community/mathlib/pull/15278) order/bounded_order: `is_well_order` instances for `with_top` and `with_bot` 
-* [PR #15636](https://github.com/leanprover-community/mathlib/pull/15636) order/bounded_order: an order is either an `order_bot` or a `no_bot_order` 
-* [PR #15341](https://github.com/leanprover-community/mathlib/pull/15341) order/bounded_order: two lemmas about the interaction between monotonicity and map with_bot/top 
-* [PR #15357](https://github.com/leanprover-community/mathlib/pull/15357) order/bounded_order: `subrelation r s ↔ r ≤ s` 
-* [PR #14195](https://github.com/leanprover-community/mathlib/pull/14195) order/bounded_order: Codisjointness 
-* [PR #15665](https://github.com/leanprover-community/mathlib/pull/15665) order/compare: general cleanup 
-* [PR #15340](https://github.com/leanprover-community/mathlib/pull/15340) order/complete_boolean_algebra: A frame is distributive 
-* [PR #15237](https://github.com/leanprover-community/mathlib/pull/15237) order/filter: add `map_neg_at_top`, change some assumptions 
-* [PR #15632](https://github.com/leanprover-community/mathlib/pull/15632) order/filter: `filter.pi` is countably generated 
-* [PR #15630](https://github.com/leanprover-community/mathlib/pull/15630) order/filter/bases: lemmas about bases of product filters 
-* [PR #15661](https://github.com/leanprover-community/mathlib/pull/15661) order/filter/basic: add `filter.has_basis.bInter_mem` 
-* [PR #15128](https://github.com/leanprover-community/mathlib/pull/15128) order/filter/basic: add `map_le_map` and `map_injective` 
-* [PR #15187](https://github.com/leanprover-community/mathlib/pull/15187) order/filter/ultrafilter: `pure`, `map`, and `comap` lemmas 
-* [PR #15432](https://github.com/leanprover-community/mathlib/pull/15432) order/hom/basic: `order_iso` of `rel_iso (<) (<)` 
-* [PR #15182](https://github.com/leanprover-community/mathlib/pull/15182) order/hom/basic: `order_iso` to `rel_iso (<) (<)` 
-* [PR #15375](https://github.com/leanprover-community/mathlib/pull/15375) order/initial_seg: Initial/principal segment from empty type 
-* [PR #15374](https://github.com/leanprover-community/mathlib/pull/15374) order/initial_seg: remove `nolint` from `initial_seg` 
-* [PR #15439](https://github.com/leanprover-community/mathlib/pull/15439) order/lattice: Congruence lemmas for `⊔` and `⊓` 
-* [PR #14789](https://github.com/leanprover-community/mathlib/pull/14789) order/lattice, data/set: some helper lemmas 
-* [PR #15136](https://github.com/leanprover-community/mathlib/pull/15136) order/lattice, order/lattice_intervals: coe inf/sup lemmas 
-* [PR #14733](https://github.com/leanprover-community/mathlib/pull/14733) order/locally_finite: make `fintype.to_locally_finite_order` computable 
-* [PR #11602](https://github.com/leanprover-community/mathlib/pull/11602) order/modular_lattice: Semimodular lattices 
-* [PR #15073](https://github.com/leanprover-community/mathlib/pull/15073) order/order_iso_nat: generalize `well_founded.monotone_chain_condition` to preorders 
-* [PR #15350](https://github.com/leanprover-community/mathlib/pull/15350) order/partition/finpartition: Bound size of a bit of `finpartition.atomise` 
-* [PR #15430](https://github.com/leanprover-community/mathlib/pull/15430) order/rel_iso: add lemmas on `rel_iso.cast` 
-* [PR #15372](https://github.com/leanprover-community/mathlib/pull/15372) order/rel_iso: relation embedding from empty type 
-* [PR #14760](https://github.com/leanprover-community/mathlib/pull/14760) order/rel_iso: two reflexive/irreflexive relations on a unique type are isomorphic 
-* [PR #15144](https://github.com/leanprover-community/mathlib/pull/15144) order/rel_iso: add `rel_iso.cast` 
-* [PR #15016](https://github.com/leanprover-community/mathlib/pull/15016) order/succ_pred: expand API on `with_bot` and `with_top` 
-* [PR #15567](https://github.com/leanprover-community/mathlib/pull/15567) order/succ_pred/basic: `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related 
-* [PR #15536](https://github.com/leanprover-community/mathlib/pull/15536) order/succ_pred/basic: `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses 
-* [PR #15001](https://github.com/leanprover-community/mathlib/pull/15001) order/succ_pred/limit: Successor and predecessor limits 
-* [PR #15581](https://github.com/leanprover-community/mathlib/pull/15581) order/upper_lower: Upper closure of a set 
-* [PR #15399](https://github.com/leanprover-community/mathlib/pull/15399) order/well_founded: typeclasses for well-founded `<` and `>` 
-* [PR #15266](https://github.com/leanprover-community/mathlib/pull/15266) order/well_founded_set: any relation is well-founded on `Ø` 
-* [PR #15678](https://github.com/leanprover-community/mathlib/pull/15678) probability/density: probability of event in uniform distribution 
-* [PR #15131](https://github.com/leanprover-community/mathlib/pull/15131) probability/independence: two tuples indexed by disjoint subsets of an independent family of r.v. are independent 
-* [PR #14909](https://github.com/leanprover-community/mathlib/pull/14909) probability/martingale: the discrete stochastic integral of a submartingale is a submartingale 
-* [PR #14737](https://github.com/leanprover-community/mathlib/pull/14737) probability/martingale: Doob's maximal inequality 
-* [PR #14932](https://github.com/leanprover-community/mathlib/pull/14932) probability/martingale: positive part of a submartingale is also a submartingale 
-* [PR #15140](https://github.com/leanprover-community/mathlib/pull/15140) probability/moments: mgf/cgf of a sum of independent random variables 
-* [PR #15129](https://github.com/leanprover-community/mathlib/pull/15129) probability/moments: Chernoff bound on the upper/lower tail of a real random variable 
-* [PR #15392](https://github.com/leanprover-community/mathlib/pull/15392) probability/strong_law: Lp version of the strong law of large numbers 
-* [PR #14331](https://github.com/leanprover-community/mathlib/pull/14331) representation_theory/Action: mapping by a monoidal functor 
-* [PR #13713](https://github.com/leanprover-community/mathlib/pull/13713) representation_theory/Rep: Rep k G ≌ Module (monoid_algebra k G) 
-* [PR #15084](https://github.com/leanprover-community/mathlib/pull/15084) representation_theory/character: formula for the dimension of the invariants in terms of the character 
-* [PR #14308](https://github.com/leanprover-community/mathlib/pull/14308) representation_theory/monoid_algebra_basis: add some API for `k[G^n]` 
-* [PR #15243](https://github.com/leanprover-community/mathlib/pull/15243) ring_theory: Formally étale/smooth/unramified morphisms are stable under base change. 
-* [PR #14348](https://github.com/leanprover-community/mathlib/pull/14348) ring_theory: the Ore localization of a ring 
-* [PR #15381](https://github.com/leanprover-community/mathlib/pull/15381) ring_theory: the integral closure `C` of `A` is Noetherian over `A` 
-* [PR #14966](https://github.com/leanprover-community/mathlib/pull/14966) ring_theory: Basic framework for classes of ring homomorphisms 
-* [PR #15064](https://github.com/leanprover-community/mathlib/pull/15064) ring_theory: Some missing lemmas 
-* [PR #15333](https://github.com/leanprover-community/mathlib/pull/15333) ring_theory/I_filtration: I-filtrations of modules. 
-* [PR #14981](https://github.com/leanprover-community/mathlib/pull/14981) ring_theory/adjoin_root: add lemmas for GCD domains 
-* [PR #15586](https://github.com/leanprover-community/mathlib/pull/15586) ring_theory/algebraic: `is_algebraic_algebra_map_iff` 
-* [PR #15424](https://github.com/leanprover-community/mathlib/pull/15424) ring_theory/bezout: Bezout domains are integrally closed 
-* [PR #15091](https://github.com/leanprover-community/mathlib/pull/15091) ring_theory/bezout: Define Bézout rings. 
-* [PR #11053](https://github.com/leanprover-community/mathlib/pull/11053) ring_theory/dedekind_domain: If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape 
-* [PR #15244](https://github.com/leanprover-community/mathlib/pull/15244) ring_theory/derivation: Derivations into square-zero ideals corresponds to liftings.  
-* [PR #15242](https://github.com/leanprover-community/mathlib/pull/15242) ring_theory/etale: Formally étale morphisms. 
-* [PR #15264](https://github.com/leanprover-community/mathlib/pull/15264) ring_theory/graded_algebra/basic: add lemma `proj_homogeneous_mul` 
-* [PR #15460](https://github.com/leanprover-community/mathlib/pull/15460) ring_theory/ideal/operations: A variant of `finsupp.total` for ideals. 
-* [PR #12812](https://github.com/leanprover-community/mathlib/pull/12812) ring_theory/integrally_closed: if x is in Frac R such that x^n is in R then x is in R 
-* [PR #15404](https://github.com/leanprover-community/mathlib/pull/15404) ring_theory/localization/basic: section of localisation of non-zero is non-zero 
-* [PR #15261](https://github.com/leanprover-community/mathlib/pull/15261) ring_theory/localization/basic: add `mk_sum` 
-* [PR #15561](https://github.com/leanprover-community/mathlib/pull/15561) ring_theory/noetherian: Finitely generated idempotent ideal is principal. 
-* [PR #15397](https://github.com/leanprover-community/mathlib/pull/15397) ring_theory/power_series/basic: Add `rescale_X` 
-* [PR #15287](https://github.com/leanprover-community/mathlib/pull/15287) ring_theory/power_series/well_known: Coefficients of sin and cos 
-* [PR #15089](https://github.com/leanprover-community/mathlib/pull/15089) ring_theory/rees_algebra: Define the Rees algebra of an ideal. 
-* [PR #15427](https://github.com/leanprover-community/mathlib/pull/15427) ring_theory/ring_hom/finite: Finite ring morphisms are stable under base change 
-* [PR #15379](https://github.com/leanprover-community/mathlib/pull/15379) ring_theory/ring_hom/finite: Finite type is a local property 
-* [PR #15512](https://github.com/leanprover-community/mathlib/pull/15512) ring_theory/tensor_product: A predicate for being the tensor product. 
-* [PR #15241](https://github.com/leanprover-community/mathlib/pull/15241) ring_theory/tensor_product: `A`-algebra structure on `A' ⊗[R] B`. 
-* [PR #15093](https://github.com/leanprover-community/mathlib/pull/15093) ring_theory/valuation: Properties of valuation rings. 
-* [PR #14896](https://github.com/leanprover-community/mathlib/pull/14896) set/intervals/monotone: add some monotonicity lemmas 
-* [PR #14989](https://github.com/leanprover-community/mathlib/pull/14989) set_theory/cardinal/ordinal: basic properties on Beth numbers 
-* [PR #15198](https://github.com/leanprover-community/mathlib/pull/15198) set_theory/cardinal/ordinal: cardinality of `α →₀ β` 
-* [PR #15367](https://github.com/leanprover-community/mathlib/pull/15367) set_theory/game/nim: make the file `noncomputable theory` 
-* [PR #14780](https://github.com/leanprover-community/mathlib/pull/14780) set_theory/game/ordinal: lemmas on `0.to_pgame` and `1.to_pgame` 
-* [PR #15255](https://github.com/leanprover-community/mathlib/pull/15255) set_theory/game/pgame: strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` 
-* [PR #15256](https://github.com/leanprover-community/mathlib/pull/15256) set_theory/game/pgame: `is_option (-x) (-y) ↔ is_option x y` 
-* [PR #15254](https://github.com/leanprover-community/mathlib/pull/15254) set_theory/game/pgame: add `equiv.comm` 
-* [PR #15533](https://github.com/leanprover-community/mathlib/pull/15533) set_theory/ordinal/arithmetic: `pred 0 = 0` 
-* [PR #15447](https://github.com/leanprover-community/mathlib/pull/15447) set_theory/ordinal/arithmetic: more log lemmas 
-* [PR #15193](https://github.com/leanprover-community/mathlib/pull/15193) set_theory/ordinal/arithmetic: tweak `type_add` and `type_mul` 
-* [PR #15174](https://github.com/leanprover-community/mathlib/pull/15174) set_theory/ordinal/arithmetic: tweak theorems about `0` and `1` 
-* [PR #15348](https://github.com/leanprover-community/mathlib/pull/15348) set_theory/ordinal/basic: dot notation lemmas + golf 
-* [PR #15152](https://github.com/leanprover-community/mathlib/pull/15152) set_theory/ordinal/basic: add `gc_ord_card` and `gci_ord_card` 
-* [PR #15194](https://github.com/leanprover-community/mathlib/pull/15194) set_theory/ordinal/basic: mark `type_fintype` as `simp` 
-* [PR #15178](https://github.com/leanprover-community/mathlib/pull/15178) set_theory/ordinal/basic: order type of naturals is `ω` 
-* [PR #15146](https://github.com/leanprover-community/mathlib/pull/15146) set_theory/ordinal/basic: basic lemmas on `ordinal.lift`  
-* [PR #15320](https://github.com/leanprover-community/mathlib/pull/15320) set_theory/zfc: ZFC sets are small types 
-* [PR #15223](https://github.com/leanprover-community/mathlib/pull/15223) set_theory/zfc: `Ø ⊆ x` 
-* [PR #15213](https://github.com/leanprover-community/mathlib/pull/15213) set_theory/zfc: `∈` is well-founded 
-* [PR #15324](https://github.com/leanprover-community/mathlib/pull/15324) set_theory/zfc: more `quotient` lemmas 
-* [PR #15214](https://github.com/leanprover-community/mathlib/pull/15214) set_theory/zfc: simp lemmas for `arity` and `const` 
-* [PR #15211](https://github.com/leanprover-community/mathlib/pull/15211) set_theory/zfc: basic lemmas on `pSet.equiv` 
-* [PR #15545](https://github.com/leanprover-community/mathlib/pull/15545) set_theory/zfc/basic: `inj` lemmas 
-* [PR #15544](https://github.com/leanprover-community/mathlib/pull/15544) set_theory/zfc/basic: `∈` is well-founded on classes 
-* [PR #15573](https://github.com/leanprover-community/mathlib/pull/15573) set_theory/zfc/basic: `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` 
-* [PR #15551](https://github.com/leanprover-community/mathlib/pull/15551) set_theory/zfc/basic: `⊆` is reflexive, transitive, antisymmetric 
-* [PR #15549](https://github.com/leanprover-community/mathlib/pull/15549) set_theory/zfc/basic: add `refl`, `symm`, `trans` attributes to `equiv` lemmas 
-* [PR #15548](https://github.com/leanprover-community/mathlib/pull/15548) set_theory/zfc/ordinal: more lemmas on transitive sets 
-* [PR #15288](https://github.com/leanprover-community/mathlib/pull/15288) set_theory/zfc/ordinal: transitive sets 
-* [PR #15498](https://github.com/leanprover-community/mathlib/pull/15498) tactic/attribute: add `expand_exists` 
-* [PR #14762](https://github.com/leanprover-community/mathlib/pull/14762) tactic/compute_degree + test/compute_degree: introduce a tactic for proving `f.(nat_)degree ≤ d` 
-* [PR #14532](https://github.com/leanprover-community/mathlib/pull/14532) tactic/congrm: add "function underscores" to `congrm` 
-* [PR #15502](https://github.com/leanprover-community/mathlib/pull/15502) tactic/ext: don't remove attr 
-* [PR #15319](https://github.com/leanprover-community/mathlib/pull/15319) tactic/linear_combination: allow linear_combination to leave goal open 
-* [PR #15284](https://github.com/leanprover-community/mathlib/pull/15284) tactic/linear_combination: add parser for `h / a` 
-* [PR #15202](https://github.com/leanprover-community/mathlib/pull/15202) tactic/lint: add a linter for `[fintype _]` assumptions 
-* [PR #14878](https://github.com/leanprover-community/mathlib/pull/14878) tactic/polyrith: a tactic using Sage to solve polynomial equalities with hypotheses 
-* [PR #15618](https://github.com/leanprover-community/mathlib/pull/15618) tactic/positivity: a tactic for proving positivity/nonnegativity 
-* [PR #15728](https://github.com/leanprover-community/mathlib/pull/15728) test/polyrith: better formatting for generated tests 
-* [PR #15641](https://github.com/leanprover-community/mathlib/pull/15641) tooplogy/metric_space/hausdorff_distance: add lemmas about `thickening` 
-* [PR #15102](https://github.com/leanprover-community/mathlib/pull/15102) topology: basic simplification lemmas for `continuous_map`s 
-* [PR #14806](https://github.com/leanprover-community/mathlib/pull/14806) topology/algebra/filter_basis: add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group 
-* [PR #15157](https://github.com/leanprover-community/mathlib/pull/15157) topology/algebra/infinite_sum: Double sum is equal to a single value 
-* [PR #15610](https://github.com/leanprover-community/mathlib/pull/15610) topology/algebra/module/finite_dimension: add 2 simp lemmas 
-* [PR #15022](https://github.com/leanprover-community/mathlib/pull/15022) topology/algebra/order: ⁻¹ continuous for linear ordered fields 
-* [PR #14889](https://github.com/leanprover-community/mathlib/pull/14889) topology/algebra/uniform_group: `uniform_group` is preserved by Inf and comap 
-* [PR #15653](https://github.com/leanprover-community/mathlib/pull/15653) topology/basic: add lemmas about `filter.lift' _ closure` 
-* [PR #15580](https://github.com/leanprover-community/mathlib/pull/15580) topology/basic: a condition implying that a sequence of functions locally stabilizes 
-* [PR #15485](https://github.com/leanprover-community/mathlib/pull/15485) topology/basic: add 2 lemmas about `locally_finite` families 
-* [PR #14036](https://github.com/leanprover-community/mathlib/pull/14036) topology/continuous_function: Any T0 space embeds in a product of copies of the Sierpinski space 
-* [PR #14724](https://github.com/leanprover-community/mathlib/pull/14724) topology/homotopy: define nth homotopy group πₙ (without the group instance) 
-* [PR #15593](https://github.com/leanprover-community/mathlib/pull/15593) topology/instances/ennreal: add `continuous(_on).ennreal_mul` 
-* [PR #15446](https://github.com/leanprover-community/mathlib/pull/15446) topology/instances/nnreal: add `can_lift C(X, ℝ) C(X, ℝ≥0)` 
-* [PR #15311](https://github.com/leanprover-community/mathlib/pull/15311) topology/local_homeomorph: "injectivity" local_homeomorph.prod 
-* [PR #15612](https://github.com/leanprover-community/mathlib/pull/15612) topology/maps: add 2 lemmas, `open function` 
-* [PR #15165](https://github.com/leanprover-community/mathlib/pull/15165) topology/maps: more `iff` lemmas 
-* [PR #14926](https://github.com/leanprover-community/mathlib/pull/14926) topology/metric_space/hausdorff_distance: Thickening a compact inside an open 
-* [PR #15591](https://github.com/leanprover-community/mathlib/pull/15591) topology/metric_space/isometry: use namespace, add lemmas 
-* [PR #15634](https://github.com/leanprover-community/mathlib/pull/15634) topology/metric_space/lipschitz: add several lemmas 
-* [PR #14965](https://github.com/leanprover-community/mathlib/pull/14965) topology/noetherian_space: Noetherian spaces 
-* [PR #15617](https://github.com/leanprover-community/mathlib/pull/15617) topology/order: upgrade some lemmas to `iff`s 
-* [PR #15490](https://github.com/leanprover-community/mathlib/pull/15490) topology/partition_of_unity: local to global 
-* [PR #15635](https://github.com/leanprover-community/mathlib/pull/15635) topology/separation: add `disjoint_nhds_nhds` 
-* [PR #15043](https://github.com/leanprover-community/mathlib/pull/15043) topology/separation: `separation_quotient α` is a T₀ space 
-* [PR #15338](https://github.com/leanprover-community/mathlib/pull/15338) topology/sets/closeds: The coframe of closed sets 
-* [PR #15118](https://github.com/leanprover-community/mathlib/pull/15118) topology/sets/compacts: prod constructions 
-* [PR #15707](https://github.com/leanprover-community/mathlib/pull/15707) topology/subset_properties: `locally_compact_space` instance for `Π` types 
-* [PR #15484](https://github.com/leanprover-community/mathlib/pull/15484) topology/support: add lemmas, fix a name 
-* [PR #15346](https://github.com/leanprover-community/mathlib/pull/15346) topology/support: tsupport of product is a subset of tsupport 
-* [PR #14892](https://github.com/leanprover-community/mathlib/pull/14892) topology/uniform_space/basic: uniform continuity from/to an infimum of uniform spaces 

From 93d73b43dbdc43db54fa2431bf82bc23d087881f Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed, 3 Aug 2022 01:51:59 +0200
Subject: [PATCH 5/5] slight improvement

---
 get_month.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/get_month.py b/get_month.py
index 365de3a1..62493821 100644
--- a/get_month.py
+++ b/get_month.py
@@ -63,7 +63,8 @@ def __init__(self, commit):
         str(now) + "\ndescription: ''\nhas_math: true\nlink: ''\nslug: month-in-mathlib-" +
         monthnames_lc[args.month] + "-" + str(args.year) +
         "\ntags: ''\ntitle: This month in mathlib (" + monthnames_uc[args.month]
-        + " " + str(args.year) + ")\ntype: text\n---\n", file=this_month_file)
+        + " " + str(args.year) + ")\ntype: text\n---\nThis month there were " +
+        number_of_commits + " PRs merged into mathlib.\n\n<!-- TEASER_END -->", file=this_month_file)
 
 for commit in sorted_commits:
     if commit.feature: