alexjbest/lastmsgs.md

## lastmsgs.md

      
    Raw
  

              lastmsgs.md
            
          
    [feat(ring_theory/dedekind_domain/selmer_group): add Selmer groups of
Dedekind domains](https://github.com/leanprover-
community/mathlib/commit/9aec1a288c6222ef5ccfd02a07155e9dd37b20de)
(mathlib#15405)
Authored-by: Multramate
[(commit)](https://github.com/leanprover-
community/mathlib/commit/9aec1a288c6222ef5ccfd02a07155e9dd37b20de)
**[feat(tactic/qify) :qify tactic](https://github.com/leanprover-

community/mathlib/commit/9fe85cd025655fc6285758c29b6a392c0fa96743)**
(mathlib#16313)
This file mainly introduces qify which casts goals or hypotheses about
natural numbers or integers to the ones about rational numbers.
Note that this file is following from zify.
This is motivated by thinking about division in natural numbers or integers.
Division in natural numbers or integers is not always working fine (e.g. (5 :
ℕ) / 2 = 2), so it's easier to work in ℚ, where division and subtraction are
well behaved.
Co-authored-by: Alex J Best
<alex.j.best@gmail.com>
Authored-by: bm221@ic.ac.uk
[(commit)](https://github.com/leanprover-
community/mathlib/commit/9fe85cd025655fc6285758c29b6a392c0fa96743)
Re qify -- could have called it ratify ;-)

I guess zify could technically have been integrate?

**[feat(algebra/char_p/mixed_char_zero): define mixed/equal characteristic

zero](https://github.com/leanprover-
community/mathlib/commit/96782a2d6dcded92116d8ac9ae48efb41d46a27c)**
(mathlib#14672)
API for equal/mixed characteristic zero with main theorem to split
propositions by characteristics.
Co-authored-by: Jon <jon.eugster@gmx.ch>

Co-authored-by: Jon Eugster
<eugster.jon@gmail.com>
Authored-by: j.eugster@sms.ed.ac.uk
[(commit)](https://github.com/leanprover-
community/mathlib/commit/96782a2d6dcded92116d8ac9ae48efb41d46a27c)
**[feat(ring_theory/filtration): Artin-Rees lemma and Krull's intersection

theorems](https://github.com/leanprover-
community/mathlib/commit/e24808b301c8ad0e27f2c63d38309ea4c5d94fb7)**
(mathlib#16000)
Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com
Authored-by: erdOne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/e24808b301c8ad0e27f2c63d38309ea4c5d94fb7)
**[feat(measure_theory/covering/density_theorem): add a version of Lebesgue's

density theorem](https://github.com/leanprover-
community/mathlib/commit/a17aefd343f32f8b9877303cb6a52f8c29bc2e93)**
(mathlib#16762)
Authored-by: ocfnash
[(commit)](https://github.com/leanprover-
community/mathlib/commit/a17aefd343f32f8b9877303cb6a52f8c29bc2e93)
**[feat(analysis/inner_product_space/gram_schmidt_ortho): generalize

orthonormal basis construction](https://github.com/leanprover-
community/mathlib/commit/96055b68cc87d46e7d2691c0152034780e7596d7)**
(mathlib#16477)
Previously, the construction gram_schmidt_orthonormal_basis performed Gram-
Schmidt orthogonalization on an existing basis to produce an orthonormal
basis. This changes it so that it outputs an orthonormal basis if the input is
any family of vectors with the right sized index set. It augments the naive
Gram-Schmidt output (an orthonormal-or-zero family of vectors, not necessarily
spanning) arbitrarily to make an orthonormal basis.
Formalized as part of the Sphere Eversion project.
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/96055b68cc87d46e7d2691c0152034780e7596d7)
**[feat(combinatorics/ssyt): add definition and basic API for semistandard

Young tableaux](https://github.com/leanprover-
community/mathlib/commit/07cdf30bd0e5335f83f83dd55b1a4f165eaedfd6)**
(mathlib#16195)
Add basic definition and initial API for semistandard Young tableaux (SSYTs).
Co-authored-by: Kyle Miller
<kmill31415@gmail.com>
Authored-by: jakelev
[(commit)](https://github.com/leanprover-
community/mathlib/commit/07cdf30bd0e5335f83f83dd55b1a4f165eaedfd6)
**[feat(algebra/indicator_function): the inverse image under a constant

indicator function has four possibilities](https://github.com/leanprover-
community/mathlib/commit/881d122b0c86b2332476cbf5150f2db06dadf9c0)**
(mathlib#16041)
The possibilities are set.univ, U, Uᶜ, ∅,
This lemma is from LTE.
Co-authored-by: Yury G. Kudryashov
<urkud@urkud.name>
Authored-by: adomani
[(commit)](https://github.com/leanprover-
community/mathlib/commit/881d122b0c86b2332476cbf5150f2db06dadf9c0)
**[fix(algebra/star/free): speedup](https://github.com/leanprover-

community/mathlib/commit/07c3cf2d851866ff7198219ed3fedf42e901f25c)**
(mathlib#16851)
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/07c3cf2d851866ff7198219ed3fedf42e901f25c)
**[feat(topology/continuous_function/ideals): construct the Galois

correspondence between closed ideals inC(X, 𝕜) and open sets in
X](https://github.com/leanprover-
community/mathlib/commit/54f74fc806aab56cdabf8f964643d80bc31b72af)**
(mathlib#16677)
For a topological ring R and a topological space X there is a Galois
connection between ideal C(X, R) and set X given by sending each I : ideal C(X, R) to {x : X | ∀ f ∈ I, f x = 0}ᶜ and mapping s : set X to the
ideal with carrier {f : C(X, R) | ∀ x ∈ sᶜ, f x = 0}, and we call these maps
continuous_map.set_of_ideal and continuous_map.ideal_of_set. As long as
R is Hausdorff, continuous_map.set_of_ideal I is open, and if, in
addition, X is locally compact, then continuous_map.set_of_ideal s is
closed.
Authored-by: j-loreaux
[(commit)](https://github.com/leanprover-
community/mathlib/commit/54f74fc806aab56cdabf8f964643d80bc31b72af)
**[feat(topology/algebra/order/left_right): left and right

limits](https://github.com/leanprover-
community/mathlib/commit/052b6cbe18941597628794e179225ff585cb93bf)**
(mathlib#16551)
We define left and right limits of a function, and prove that a monotone
function is continuous at a point if and only if its left and right limits
coincide.
We also refactor the file on Stieltjes functions using this general definition
instead of the ad hoc definition that is currently used.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/052b6cbe18941597628794e179225ff585cb93bf)
**[feat(probability/variance): introduceℝ≥0∞-valued

variance](https://github.com/leanprover-
community/mathlib/commit/85453a2a14be8da64caf15ca50930cf4c6e5d8de)**
(mathlib#16730)
This PR introduces ℝ≥0∞-valued variance and define the real-valued variance
in terms of it.
Authored-by: JasonKYi
[(commit)](https://github.com/leanprover-
community/mathlib/commit/85453a2a14be8da64caf15ca50930cf4c6e5d8de)
**[feat(measure_theory/covering): improve Vitali families and Lebesgue density

theorem](https://github.com/leanprover-
community/mathlib/commit/a67fbae61f4021038cad203c89af722c3aca992a)**
(mathlib#16830)
#16762 has shown
weaknesses of our current implementation of Vitali families. Notably, it
enforces that the sets based at x all contain x, which is not natural for
some applications.
We refactor Vitali families to solve this issue. Here are the main changes:

in the definition of Vitali families, in the covering property it is now allowed to use several sets based at the same point (which means that the covering is not indexed by α but by α × set α)
We modify the Vitali covering theorem to deal with general indexed families, to fit in this framework.
This makes it possible to define better Vitali families for doubling measures. In particular, for any K, we define a Vitali family such that the sets based at x contain all balls closed_ball y r when dist x y ≤ K * r.
This gives a better Lebesgue density theorem, solving the issue pointed out in #16762

Co-authored-by: sgouezel <sebastien.gouezel@univ-
rennes1.fr>
Authored-by: ocfnash
[(commit)](https://github.com/leanprover-
community/mathlib/commit/a67fbae61f4021038cad203c89af722c3aca992a)
**[feat(algebra/order/ring): Non-cancellative ordered

semirings](https://github.com/leanprover-
community/mathlib/commit/f5a600f8102c8bfdbd22781968a20a539304c1b4)**
(mathlib#16172)
Historical background

This tackles a problem that we have had for six years
(#2697 for its
move to mathlib, before it was in core): ordered_semiring assumes that
addition and multiplication are strictly monotone.
This led to weirdness within the algebraic order hierarchy:

ennreal/ereal/enat needed custom lemmas (∞ + 0 = ∞ = ∞ + 1, 1 * ∞ = ∞ = 2 * ∞).
A canonically_ordered_comm_semiring was not an ordered_comm_semiring!

What this PR does

This PR solves the problem minimally by renaming ordered_(comm_)semiring to
strict_ordered_(comm_)semiring and adding a new class
ordered_(comm_)semiring that doesn't assume strict monotonicity of addition
and multiplication but only monotonicity:
class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_le_mul_of_nonneg_left  : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)

class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α

class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α

class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)

class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α

class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)

class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α

Whatever happened to the decidable lemmas?

Scrolling through the diff, you will see that only one lemma in the
decidable namespace out of many survives this PR. Those lemmas were
originally meant to avoid using choice in the proof of nat and int lemmas.
The need for decidability originated from the proofs of
mul_le_mul_of_nonneg_left/mul_le_mul_of_nonneg_right.
protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
  (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
begin
  by_cases ba : b ≤ a, { simp [ba.antisymm h₁] },
  by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] },
  exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le,
end

Now that these are fields to ordered_semiring, they are already choice-free.
Instead, choice is now used in showing that an ordered_cancel_semiring is an
ordered_semiring.
@[priority 100] -- see Note [lower instance priority]
instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α :=
{ mul_le_mul_of_nonneg_left := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_left hab hc).le }
  end,
  mul_le_mul_of_nonneg_right := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_right hab hc).le }
  end,
  ..‹ordered_cancel_semiring α› }

It seems unreasonable to make that instance depend on @decidable_rel α (≤)
even though it's only needed for the proofs.
Other changes

To have some lemmas in the generality of the new ordered_semiring, I needed
a few new lemmas:

bit0_mono
bit0_strict_mono

It was also simpler to golf analysis.special_functions.stirling using
positivity rather than fixing it so I introduce the following (simple)
positivity extensions:

positivity_succ
positivity_factorial
positivity_asc_factorial

Authored-by: YaelDillies
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f5a600f8102c8bfdbd22781968a20a539304c1b4)
**[feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic

as a module to the exterior algebra](https://github.com/leanprover-
community/mathlib/commit/446eb51ce0a90f8385f260d2b52e760e2004246b)**
(mathlib#11468)
The key result here is
/-- The module isomorphism to the exterior algebra -/
def equiv_exterior [invertible (2 : R)] : clifford_algebra Q ≃ₗ[R] exterior_algebra R M :=

There are a handful of intermediate definitions that are needed to get here
that are missing lots of useful (but difficult) API lemmas, but I don't expect
to have time to address those for a while.
Probably the main missing result is that equiv_exterior preserves reversion.
Authored-by: eric-wieser
[(commit)](https://github.com/leanprover-
community/mathlib/commit/446eb51ce0a90f8385f260d2b52e760e2004246b)
**[perf(topology/sheaves/presheaf_of_functions):

speedups](https://github.com/leanprover-
community/mathlib/commit/6c31dd6563a3745bf8e0b80bdd077167583ebb8f)**
(mathlib#16873)
Speed upCommRing_yoneda (which caused [a bors
failure](https://github.com/leanprover-
community/mathlib/actions/runs/3211416019/jobs/5249570763)) from >20s to <2.5s
by filling in automatic fields. (merged in another PR)
Speed up presheaf_to_Types from 13.3s to 0.3s and presheaf_to_Type from 4s
to 0.1s by filling in automatic fields.
Authored-by: alreadydone
[(commit)](https://github.com/leanprover-
community/mathlib/commit/6c31dd6563a3745bf8e0b80bdd077167583ebb8f)
**[chore(data/int/gcd): streamline imports](https://github.com/leanprover-

community/mathlib/commit/103252aeb19cd2de4ab2ad5fa0ad3539faf14560)**
(mathlib#16811)
The file on gcds of integers is fundamentally very elementary, but it
contained two lemmas about prime numbers, and data.nat.prime seems to import
everything (modules! half the order library!).
Co-authored-by: Andrew Yang
<the.erd.one@gmail.com>

Co-authored-by: Yaël Dillies
<yael.dillies@gmail.com>

Co-authored-by: Joël Riou <joel.riou@universite-paris-
saclay.fr>

Co-authored-by: Junyan Xu
<junyanxumath@gmail.com>
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/103252aeb19cd2de4ab2ad5fa0ad3539faf14560)
**[feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is

doubling](https://github.com/leanprover-
community/mathlib/commit/09b58946c2bbda1b73165474c0c565d40a13cbec)**
(mathlib#16885)
Also split the file measure_theory/covering/density_theorem in two, to avoid
importing all the differentiation theory into haar_lebesgue.lean.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/09b58946c2bbda1b73165474c0c565d40a13cbec)
**[feat(topology/algebra/group): discrete subgroup acts properly

discontinuously](https://github.com/leanprover-
community/mathlib/commit/c476f200c379dbbc8ff5aaac5390ed69ee582099)**
(mathlib#16593)
A discrete subgroup of a topological group acts properly discontinuously on
the left and on the right. Here discrete means finite intersection with any
compact subset.
Co-authored-by: Alex Kontorovich
58564076+AlexKontorovich@users.noreply.github.com
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/c476f200c379dbbc8ff5aaac5390ed69ee582099)
**[feat(algebra/algebra/basic): make algebra_map a low prio

has_lift_t](https://github.com/leanprover-
community/mathlib/commit/d840349db150e13809a02a4f3021cbf0850c9b1c)**
(mathlib#16567)
Make algebra_map a coercion (or more precisely a has_lift_t). I have an
example where making algebra_map a coercion makes a lot of code far less messy
and I'm wondering whether it's a good idea in general.
Co-authored-by: Vierkantor
<vierkantor@vierkantor.com>
Authored-by: kbuzzard
[(commit)](https://github.com/leanprover-
community/mathlib/commit/d840349db150e13809a02a4f3021cbf0850c9b1c)
**[feat(analysis/calculus): bounded variation

functions](https://github.com/leanprover-
community/mathlib/commit/aadde30334fb810adb293b0d895ce78ad7e394a5)**
(mathlib#16683)
We define bounded variation functions, and prove that such a function is the
difference of two monotone functions. We also show that Lipschitz functions
have bounded variation.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/aadde30334fb810adb293b0d895ce78ad7e394a5)
**[feat(analysis/analytic/uniqueness): two analytic functions that coincide

locally coincide globally](https://github.com/leanprover-
community/mathlib/commit/476f28f8481aea7227a6acc2888b76b4d5188dc3)**
(mathlib#16723)
Higher dimensional version of [#16489](https://github.com/leanprover-
community/mathlib/pull/16489).
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/476f28f8481aea7227a6acc2888b76b4d5188dc3)
**[feat(measure_theory/integral/riesz_markov_kakutani): begin construction of

content for Riesz-Markov-Kakutani](https://github.com/leanprover-
community/mathlib/commit/7bbc52b758daaa5dbe02d472dd22e1f8e3af42bd)**
(mathlib#16367)
Begin construction of content for Riesz-Markov-Kakutani
Construct a map on the compact sets and prove monotonicity and subadditivity.
Co-authored-by: ReimannJ 105789986+ReimannJ@users.noreply.github.com
Authored-by: ReimannJ
[(commit)](https://github.com/leanprover-
community/mathlib/commit/7bbc52b758daaa5dbe02d472dd22e1f8e3af42bd)
**[feat(topology/instances/add_circle): the additive circleℝ / (a ∙ ℤ) is

normal (T4) and second-countable](https://github.com/leanprover-
community/mathlib/commit/0fbd703b3da57ec0476dc1bc06931994055ae2f5)**
(mathlib#16594)
The T4 fact is in mathlib already, via the normed_add_comm_group instance on
ℝ / (a ∙ ℤ), but this gives it earlier in the hierarchy.
Co-authored-by: Alex Kontorovich
58564076+AlexKontorovich@users.noreply.github.com
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/0fbd703b3da57ec0476dc1bc06931994055ae2f5)
**[perf(algebra/category/Module/monoidal): fix

timeout](https://github.com/leanprover-
community/mathlib/commit/556f35346ebc651dbc65ae6deb3a031f3d399e9d)**
(mathlib#16903)
elaboration of category_theory.monoidal_preadditive took 23.2s -> 2.93s

elaboration of category_theory.monoidal_linear took 12.5s -> 2.89s
[timeout in last bors batch](https://github.com/leanprover-
community/mathlib/actions/runs/3223730534/jobs/5274107482)
Authored-by: alreadydone
[(commit)](https://github.com/leanprover-
community/mathlib/commit/556f35346ebc651dbc65ae6deb3a031f3d399e9d)
**[feat(measure_theory/integral/periodic): relate integrals overadd_circle

with integrals upstairs in ℝ](https://github.com/leanprover-
community/mathlib/commit/f1138dc36c9712ebe491a4002704e89cdc597b86)**
(mathlib#16836)
Prove that the covering map from ℝ to add_circle is measure-preserving,
with respect to Lebesgue measure restricted to an interval (upstairs) and Haar
measure (downstairs). As corollaries, lemmas relating the various integrals
upstairs and downstairs.
Co-authored-by: Alex Kontorovich
58564076+AlexKontorovich@users.noreply.github.com
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f1138dc36c9712ebe491a4002704e89cdc597b86)
**[feat(analysis/inner_product_space/orientation): volume

form](https://github.com/leanprover-
community/mathlib/commit/265fe3d814d6eb043ec6c269196df77f30c605fc)**
(mathlib#16487)
Construct the volume form, a uniquely-determined top-dimensional alternating
form on an oriented real inner product space.
Formalized as part of the Sphere Eversion project.
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/265fe3d814d6eb043ec6c269196df77f30c605fc)
**[feat(linear_algebra/matrix): Schur

complement](https://github.com/leanprover-
community/mathlib/commit/68ead6e664f4a86b2405055689683ebdcf44c177)**
(mathlib#15270)
If a matrix A is positive definite, then [A B; Bᴴ D] is postive
semidefinite if and only if D - Bᴴ A⁻¹ B is postive semidefinite.
Authored-by: abentkamp
[(commit)](https://github.com/leanprover-
community/mathlib/commit/68ead6e664f4a86b2405055689683ebdcf44c177)
**[feat(analysis/calculus/monotone): a monotone function is differentiable

almost everywhere](https://github.com/leanprover-
community/mathlib/commit/c9f6b6f0f91743b1661758867b960d91e2d4b2b8)**
(mathlib#16549)
The proof is an almost direct consequence of results on differentiation of
measures that are already in mathlib.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/c9f6b6f0f91743b1661758867b960d91e2d4b2b8)
**[feat(measure_theory/covering/differentiation): Lebesgue differentiation

theorem](https://github.com/leanprover-
community/mathlib/commit/f45d33795824b768fd642b7e89d9e37e101649db)**
(mathlib#16906)
Given a doubling measure, then at almost every x the average of an
integrable function on closed_ball x r converges to f x as r tends to
zero (this is Lebesgue differentiation theorem). We give a version of this
theorem for general Vitali families, and the concrete application to doubling
measures.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f45d33795824b768fd642b7e89d9e37e101649db)
**[feat(geometry/euclidean/basic):concyclic](https://github.com/leanprover-

community/mathlib/commit/8f82d25e27b93224d123fbf1c73d686ea1cb3666)**
(mathlib#16927)
Define a set of points to be concyclic if it is cospherical and coplanar. I
don't expect that much use of this definition, as opposed to the separate
cospherical and coplanar pieces, in mathlib, but it's intended to allow
formal statements of results involving concyclic points that correspond more
closely to the informal statements.
Authored-by: jsm28
[(commit)](https://github.com/leanprover-
community/mathlib/commit/8f82d25e27b93224d123fbf1c73d686ea1cb3666)
**[feat(analysis/normed_space/lp_equiv): equivalences betweenlp and pi_Lp,

bounded_continuous_function](https://github.com/leanprover-
community/mathlib/commit/91b5bdde5c5078b74a44c52e886f9c5904ce6590)**
(mathlib#15872)
This adds a new file for equivalences between various L^p spaces. We do this
in a new file instead of analysis/normed_space/lp_space in order to minimize
imports. We begin by establishing the equivalence between lp and pi_Lp
when the index type is a fintype, and then proceed to recognize the
equivalence between lp (for p = ∞) and bounded_continuous_function when
the codomain has various algebraic structures.

 depends on: #15833
 depends on: #15852

Authored-by: j-loreaux
[(commit)](https://github.com/leanprover-
community/mathlib/commit/91b5bdde5c5078b74a44c52e886f9c5904ce6590)
**[feat(analysis/bounded_variation): functions of bounded variation are ae

differentiable](https://github.com/leanprover-
community/mathlib/commit/71429ce7c6fa5b0f069ea89c05c0bac8b073a5a6)**
(mathlib#16680)
We define functions of bounded variation. We show that such functions are a
difference of monotone functions, and deduce that they are differentiable
almost everywhere. This applies in particular to Lipschitz functions.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/71429ce7c6fa5b0f069ea89c05c0bac8b073a5a6)
**[feat(analysis/normed_space/star/gelfand_duality): functoriality

ofcharacter_space ℂ](https://github.com/leanprover-
community/mathlib/commit/e0ce21862273a48e47abe598035d4d043e3e3ecb)**
(mathlib#16835)
This is one of the two contravariant functors involved in Gelfand duality.
Authored-by: j-loreaux
[(commit)](https://github.com/leanprover-
community/mathlib/commit/e0ce21862273a48e47abe598035d4d043e3e3ecb)
**[feat(probability/independence): Kolmogorov's 0-1

law](https://github.com/leanprover-
community/mathlib/commit/da4010c2a5121b5284c21c732a6ed43633713336)**
(mathlib#16648)
We prove that any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1.
Co-authored-by: Rémy Degenne
<remydegenne@gmail.com>

Co-authored-by: sgouezel <sebastien.gouezel@univ-
rennes1.fr>
Authored-by: RemyDegenne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/da4010c2a5121b5284c21c732a6ed43633713336)
**[feat(analysis/complex/open_mapping): the open mapping thm for holomorphic

functions](https://github.com/leanprover-
community/mathlib/commit/5c19b83b7da2964a07475ae7c3182368921381c0)**
(mathlib#16780)
Co-authored-by: sgouezel <sebastien.gouezel@univ-
rennes1.fr>

Co-authored-by: Johan Commelin
<johan@commelin.net>
Authored-by: vbeffara
[(commit)](https://github.com/leanprover-
community/mathlib/commit/5c19b83b7da2964a07475ae7c3182368921381c0)
rss-bot said:


[chore(algebra/group/*): attribute copyright properly, correct instance
names](https://github.com/leanprover-
community/mathlib/commit/372310d0bfda6bf7e3406fe1bf57d154ca3191a0)
([mathlib#16967](https://github.com/leanprover-
community/mathlib/pull/16967))
#16847 copied
over the copyright from algebra.group.basic without actually attributing
things properly.
All the material in algebra.group.commutator is from
#12309 and the
material is mostly from [#16122](https://github.com/leanprover-
community/mathlib/pull/16122) with some dating back from
#8564
Also fix order_dual.has_pow being additivized as order_dual.has_nsmul
rather than order_dual.has_smul.
Authored-by: YaelDillies
[(commit)](https://github.com/leanprover-
community/mathlib/commit/372310d0bfda6bf7e3406fe1bf57d154ca3191a0)

Thanks, @Yaël Dillies. :-) I think I'm going to continue with the approach
that if you contribute to a large file, you take your chances with author
attribution. Keeping track of this stuff is fine if someone wants to do it,
but it shouldn't ever be an obstacle to refactoring.
Thanks for catching order_dual.has_nsmul!
**[feat(topology/metric_space/infsep): Add "infimum

separation".](https://github.com/leanprover-
community/mathlib/commit/5316314b553dcf8c6716541851517c1a9715e22b)**
(mathlib#15689)
Informally, this is the "minimum distance", though "minimum" makes sense
mainly only in the finite context. This is analogous to diam in some sense. We
provide finset and set versions for both the emetric and metric cases.
We generally try to have the analogous lemmas that diam has, and any other
useful utility lemmas to allow for the use of the definition without unpacking
it.
Authored-by: linesthatinterlace
[(commit)](https://github.com/leanprover-
community/mathlib/commit/5316314b553dcf8c6716541851517c1a9715e22b)
**[feat(number_theory/kummer_dedekind): define conductor and add basic API

plus theorem](https://github.com/leanprover-
community/mathlib/commit/813725f8aa036240cc9dd1c4b05e700ba97f8f0d)**
(mathlib#16833)
In this PR we define the conductor ideal and prove some basic results about
it.

In a later PR ([#16870](https://github.com/leanprover-
community/mathlib/pull/16870)), these will be used to prove the Dedekind-
Kummer theorem in full generality.
Co-authored-by: Paul Lezeau
<paul.lezeau@gmail.com>
Authored-by: Paul-Lez
[(commit)](https://github.com/leanprover-
community/mathlib/commit/813725f8aa036240cc9dd1c4b05e700ba97f8f0d)
**[feat(ring_theory/discrete_valuation_ring): add

not_is_field](https://github.com/leanprover-
community/mathlib/commit/7cc9c7ad820f6ce591e92b4a24f90769edd899b2)**
(mathlib#16979)
A discrete valuation ring is not a field.
Authored-by: mariainesdff
[(commit)](https://github.com/leanprover-
community/mathlib/commit/7cc9c7ad820f6ce591e92b4a24f90769edd899b2)
**[chore(algebra/*): mark frozen files that have been ported to

mathlib4](https://github.com/leanprover-
community/mathlib/commit/97bdf517581e1ed85bb3a6e82ad0f78bf05fd4fc)**
(mathlib#17039)
This is chiefly a proposal that we get started marking files as frozen, and a
proposal for a specific format.
Once we settle on what gets written here, we should add some CI that adds a
special label to any PR modifying a frozen file.
Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/97bdf517581e1ed85bb3a6e82ad0f78bf05fd4fc)
I've switched the wiki to codeblock formatting now

Ugh, premature again, I confused the commits

**[feat(representation_theory/group_cohomology_resolution): add exactness

properties of resolution](https://github.com/leanprover-
community/mathlib/commit/618ea3d5c99240cd7000d8376924906a148bf9ff)**
(mathlib#17005)
Co-authored-by: Amelia Livingston
40745104+101damnations@users.noreply.github.com
Authored-by: 101damnations@github.com
[(commit)](https://github.com/leanprover-
community/mathlib/commit/618ea3d5c99240cd7000d8376924906a148bf9ff)
**[feat(topology/covering): Define covering

spaces](https://github.com/leanprover-
community/mathlib/commit/42d514e8ed77b59647d5d96a56740e8f208c6312)**
(mathlib#16087)
This PR adds a definition of covering spaces.
We don't want to have to specify a constant index set I, and we don't want
to say "there exists an index set I : Type u such that f ⁻¹' U is
homeomorphic to I × U" (annoying universe issues). Instead, we can use the
preimage of any point as our index set.
Supersedes [#15276](https://github.com/leanprover-
community/mathlib/pull/15276), where @alreadydone suggested that I drop the
surjectivity assumption.
Authored-by: tb65536
[(commit)](https://github.com/leanprover-
community/mathlib/commit/42d514e8ed77b59647d5d96a56740e8f208c6312)
**[feat(tactic/rcases.lean):@⟨p1, p2⟩ patterns in

rcases](https://github.com/leanprover-
community/mathlib/commit/356447fe00e75e54777321045cdff7c9ea212e60)**
(mathlib#16617)
This PR implements the syntax @pat inside rcases patterns, before tuple
patterns. It has the effect of making the patterns line up with all arguments
to the constructor, rather than just the explicit ones. The original behavior
is equivalent to using @ everywhere.
Authored-by: digama0
[(commit)](https://github.com/leanprover-
community/mathlib/commit/356447fe00e75e54777321045cdff7c9ea212e60)
**[feat(number_theory/padics/padic_numbers): add is_fraction_ring

instance](https://github.com/leanprover-
community/mathlib/commit/082350f297d0099c30e4a90af4ed1259ec7e912b)**
(mathlib#16981)
ℚ_[p] is the fraction ring of ℤ_[p].
Authored-by: mariainesdff
[(commit)](https://github.com/leanprover-
community/mathlib/commit/082350f297d0099c30e4a90af4ed1259ec7e912b)
**[feat(ring_theory/derivation): The Kähler differential module is

functorial](https://github.com/leanprover-
community/mathlib/commit/cceedbca260b7ea0e5ed4da0589e922f9f3774cf)**
(mathlib#17018)
Co-authored-by: Alex J Best
<alex.j.best@gmail.com>

Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com
Authored-by: erdOne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/cceedbca260b7ea0e5ed4da0589e922f9f3774cf)
**[feat(src/algebraic_geometry/morphisms/quasi_separated): Define quasi-

separated morphisms.](https://github.com/leanprover-
community/mathlib/commit/558f58304491aabb1373c346910051f2b24538e2)**
(mathlib#17080)
Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com
Authored-by: erdOne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/558f58304491aabb1373c346910051f2b24538e2)
**[feat(algebraic_geometry/morphisms/universally_closed): Define universally

closed morphism between schemes](https://github.com/leanprover-
community/mathlib/commit/434e2fd21c1900747afc6d13d8be7f4eedba7218)**
(mathlib#17117)
Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com
Authored-by: erdOne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/434e2fd21c1900747afc6d13d8be7f4eedba7218)
Aargh data.sigma.basic is surely my fault -- I could have sworn I opened a

PR for that! ... yeah this is [#17082](https://github.com/leanprover-
community/mathlib/pull/17082), which failed to compile because of an unrelated
issue and I didn't notice because I never check github :-( Can someone merge
#17082?
**[feat(analysis/schwartz_space): Delta

distribution](https://github.com/leanprover-
community/mathlib/commit/b251b44a0a61d4a14ced401ddf7d60b8a8b0c7d0)**
(mathlib#16638)
Define the delta distribution
Authored-by: mcdoll
[(commit)](https://github.com/leanprover-
community/mathlib/commit/b251b44a0a61d4a14ced401ddf7d60b8a8b0c7d0)
**[feat(data/nat/choose/multinomial): add multinomial

theorem](https://github.com/leanprover-
community/mathlib/commit/c9e2f05526bc6cc70578efcf0cda7d7fa261dab1)**
(mathlib#16317)
Proof by induction on the number of summands. finset.sym is used to sum over.
It means we have access to the finset tooling to rewrite it, and it's one of
the more direct ways of expressing it.
Co-authored-by: Pim Otte <potte@quintor.nl>

Co-authored-by: Junyan Xu
<junyanxumath@gmail.com>

Co-authored-by: Junyan Xu
<junyanxu.math@gmail.com>
Authored-by: pimotte
[(commit)](https://github.com/leanprover-
community/mathlib/commit/c9e2f05526bc6cc70578efcf0cda7d7fa261dab1)
**[feat(topology/continuous_function/ideals): maximal ideals correspond to

(complements of) singletons](https://github.com/leanprover-
community/mathlib/commit/63ff453230aa38963a3d9d4565e26e8ab72aec7c)**
(mathlib#16719)
This establishes the correspondence between maximal ideals of C(X, 𝕜) (where
X is compact Hausdorff and is_R_or_C 𝕜) and the complements of singletons
in X. This allows for the proof that the natural map from X to
character_space 𝕜 C(X, 𝕜) is a homeomorphism.

 depends on: #16709
 depends on: #16713
 depends on: #16714
 depends on: #16677
 depends on: #16663
 depends on: #16721
 depends on: #16722
 depends on: #16801

Authored-by: j-loreaux
[(commit)](https://github.com/leanprover-
community/mathlib/commit/63ff453230aa38963a3d9d4565e26e8ab72aec7c)
**[feat(category_theory/localization): basic API for localization of

categories](https://github.com/leanprover-
community/mathlib/commit/1a5e56f2166e4e9d0964c71f4273b1d39227678d)**
(mathlib#16969)
In this PR, the basic API for the localization of categories is introduced. If
a functor L : C ⥤ D is a localization functor for W : morphism_property C,
we shall say that a functor F' : D ⥤ E lifts a functor F : C ⥤ E if an
isomorphism L ⋙ F' ≅ F is given: this is the class [lifting L W F F']. The
basic API for lifting of functors and lifting of natural transformations is
included.
Authored-by: joelriou
[(commit)](https://github.com/leanprover-
community/mathlib/commit/1a5e56f2166e4e9d0964c71f4273b1d39227678d)
**[feat(measure_theory/measure/content): regular

contents](https://github.com/leanprover-
community/mathlib/commit/90cde5e1d2a592acc40b681eeaf66821c571fe2c)**
(mathlib#16289)
Define regular contents and prove that regular contents agree with their
induced measures on compact sets.
Co-authored-by: ReimannJ 105789986+ReimannJ@users.noreply.github.com

Co-authored-by: Floris van Doorn
<fpvdoorn@gmail.com>
Authored-by: ReimannJ
[(commit)](https://github.com/leanprover-
community/mathlib/commit/90cde5e1d2a592acc40b681eeaf66821c571fe2c)
**[feat(data/bool/basic): add several lemmas](https://github.com/leanprover-

community/mathlib/commit/44c394bb075cca490529ba6e1819351a4fcc5bec)**
(mathlib#17153)
Also rename bool.bnot_false/bool.bnot_true to more predictable names
bool.bnot_ff/bool.bnot_tt.
Authored-by: urkud
[(commit)](https://github.com/leanprover-
community/mathlib/commit/44c394bb075cca490529ba6e1819351a4fcc5bec)
**[feat(analysis/normed_space/star/gelfand_duality): realize the Gelfand

transform as astar_alg_equiv](https://github.com/leanprover-
community/mathlib/commit/30415257ce7ca75cb0dce7f7006137678ab2a666)**
(mathlib#17167)
Authored-by: j-loreaux
[(commit)](https://github.com/leanprover-
community/mathlib/commit/30415257ce7ca75cb0dce7f7006137678ab2a666)
**[src(dynamics/ergodic/ergodic): define ergodic maps /

measures](https://github.com/leanprover-
community/mathlib/commit/9743845b0c20ac6b6763f5d0bfdd6f35eeff7db0)**
(mathlib#17046)
Authored-by: ocfnash
[(commit)](https://github.com/leanprover-
community/mathlib/commit/9743845b0c20ac6b6763f5d0bfdd6f35eeff7db0)
**[chore(bar): drop empty file](https://github.com/leanprover-

community/mathlib/commit/ca53494a1b3674b73096e1511dec060f355a0fbc)**
(mathlib#17208)
Accidentally included in [#17137](https://github.com/leanprover-
community/mathlib/pull/17137)
Authored-by: ocfnash
[(commit)](https://github.com/leanprover-
community/mathlib/commit/ca53494a1b3674b73096e1511dec060f355a0fbc)
**[feat(tactic/push_neg): #push_neg user

command](https://github.com/leanprover-
community/mathlib/commit/822af854c68cce8311a854e13977975641fb3430)**
(mathlib#16775)
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/822af854c68cce8311a854e13977975641fb3430)
**[feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution

existence theorem](https://github.com/leanprover-
community/mathlib/commit/f97c17d51a55d363d6508a7ccb8725c0df260008)**
(mathlib#16348)
We add some corollaries to the existence theorem of solutions to autonomous
ODEs (Picard-Lindelöf / Cauchy-Lipschitz theorem).

is_picard_lindelof: Predicate for the very long hypotheses of the Picard-Lindelöf theorem.

When applying exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous directly to unite with a goal, Lean introduces a long list of goals with many meta-variables. The predicate makes the proof of these hypotheses more manageable.
Certain variables in the hypotheses, such as the Lipschitz constant, are often obtained from other facts non-constructively, so it is less convenient to directly use them to satisfy hypotheses (needing Exists.some). We avoid this problem by stating these non-Prop hypotheses under ∃.


Solution f exists on any subset s of some closed interval, where the derivative of f is defined by the value of f within s only.
Solution f exists on any open subset s of some closed interval.
There exists ε > 0 such that a solution f exists on (t₀ - ε, t₀ + ε).
As a simple example, we show that time-independent, locally continuously differentiable ODEs satisfy is_picard_lindelof and hence a solution exists within some open interval.

Authored-by: winstonyin
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f97c17d51a55d363d6508a7ccb8725c0df260008)
**[chore(*): consistently use R[X] notation for

polynomials](https://github.com/leanprover-
community/mathlib/commit/62c0a4ef1441edb463095ea02a06e87f3dfe135c)**
(mathlib#17044)
Consistently use R[X] in favour of polynomial R. The exceptions that I've
left as is are the cases where R itself includes an identifier or more
brackets.
Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/62c0a4ef1441edb463095ea02a06e87f3dfe135c)
**[chore(measure_theory/measure/finite_measure_weak_convergence): Change to

probability theory notations.](https://github.com/leanprover-
community/mathlib/commit/8315f58ea7ded4917347d7bad0939f6081e5256b)**
(mathlib#17231)
Change notations of the underlying measurable spaces from α to Ω.
Authored-by: kkytola
[(commit)](https://github.com/leanprover-
community/mathlib/commit/8315f58ea7ded4917347d7bad0939f6081e5256b)
**[feat(probability/borel_cantelli): the second Borel-Cantelli

lemma](https://github.com/leanprover-
community/mathlib/commit/1e7dab978c588198a170835fefd3c291849be8e0)**
(mathlib#16882)
Co-authored-by: JasonKYi
<kexing.ying19@imperial.ac.uk>

Co-authored-by: RemyDegenne
<Remydegenne@gmail.com>

Co-authored-by: Kexing Ying
<kexing.ying19@imperial.ac.uk>
Authored-by: JasonKYi
[(commit)](https://github.com/leanprover-
community/mathlib/commit/1e7dab978c588198a170835fefd3c291849be8e0)
**[feat(data/real/ennreal): Positivity extension

forennreal.of_real](https://github.com/leanprover-
community/mathlib/commit/1ab3ae0371bfd3005b9b03c752ec3d230f433a7e)**
(mathlib#16955)
and three easy lemmas
Authored-by: YaelDillies
[(commit)](https://github.com/leanprover-
community/mathlib/commit/1ab3ae0371bfd3005b9b03c752ec3d230f433a7e)
**[feat(category_theory/triangulated): changing namespaces, introducing

triangulated categories](https://github.com/leanprover-
community/mathlib/commit/19786714ebe478f40b503acb4705fb058ba47303)**
(mathlib#17284)
This PR moves the namespace category_theory.triangulated.pretriangulated to
category_theory.pretriangulated, and introduces triangulated categories.
Co-authored-by: Joël Riou 37772949+joelriou@users.noreply.github.com
Authored-by: joelriou
[(commit)](https://github.com/leanprover-
community/mathlib/commit/19786714ebe478f40b503acb4705fb058ba47303)
**[feat(representation_theory/fdRep): Schur's

lemma](https://github.com/leanprover-
community/mathlib/commit/b9430470125765e888faffcc143338957da7175e)**
(mathlib#13794)
In fact, we've had Schur's lemma in mathlib for over a year, since
#7366, but this
was stated very abstractly: for any linear category over an algebraically
closed field with finite dimensional hom spaces, and kernels.
Finally, fdRep k G satisfies all those hypotheses, so we can use Schur's
lemma!
Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/b9430470125765e888faffcc143338957da7175e)
**[refactor(analysis/complex): use Liouville to prove algebraic

closedness](https://github.com/leanprover-
community/mathlib/commit/3642cbedda7d52bd9d5a5ad6baca763661e259c5)**
(mathlib#17343)
To avoid cyclic import, one proof in
analysis/special_functions/trigonometric/complex is changed.
Inspired by [#17329](https://github.com/leanprover-
community/mathlib/pull/17329).
Authored-by: alreadydone
[(commit)](https://github.com/leanprover-
community/mathlib/commit/3642cbedda7d52bd9d5a5ad6baca763661e259c5)
**[feat(topology/algebra/module/strong_operator,

analysis/normed_space/operator_norm): strong operator
topology](https://github.com/leanprover-
community/mathlib/commit/b916d59f44e28190425c5d227e8114e2b2c0da53)**
(mathlib#16053)
Authored-by: ADedecker
[(commit)](https://github.com/leanprover-
community/mathlib/commit/b916d59f44e28190425c5d227e8114e2b2c0da53)
Why is the above commit empty?

[co-authored-by.png](/user_uploads/3121/KHK3Ap-hXaK6L2dghZZtqrVd/co-authored-

by.png)
![](/user_uploads/3121/KHK3Ap-hXaK6L2dghZZtqrVd/co-authored-
by.png)
**[refactor(*): supremum of several recent refactoring

PRs](https://github.com/leanprover-
community/mathlib/commit/f7707875544ef1f81b32cb68c79e0e24e45a0e76)**
(mathlib#17381)
This is the supremum of

#17376
#17375
#17374
#17362
#17355
#17349
#17347
#17338
#17336

with imports fixed up to accommodate all the overlapping changes to imports.
Co-authored-by: Yury G. Kudryashov
<urkud@urkud.name>

Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>

Co-authored-by: Yaël Dillies
<yael.dillies@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f7707875544ef1f81b32cb68c79e0e24e45a0e76)
**[refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421

#17422 #17423 #17427 #17430](https://github.com/leanprover-
community/mathlib/commit/47b51515e69f59bca5cf34ef456e6000fe205a69)**
(mathlib#17424)
Co-authored-by: Yury G. Kudryashov
<urkud@urkud.name>

Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>

Co-authored-by: Yaël Dillies
<yael.dillies@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/47b51515e69f59bca5cf34ef456e6000fe205a69)
**[feat(representation_theory/character): orthogonality of

characters](https://github.com/leanprover-
community/mathlib/commit/55b3f8206b8596db8bb1804d8a92814a0b6670c9)**
(mathlib#16043)
Orthogonality of characters for representations of finite groups
Co-authored-by: antoinelab01 66086247+antoinelab01@users.noreply.github.com
Authored-by: antoinelab01
[(commit)](https://github.com/leanprover-
community/mathlib/commit/55b3f8206b8596db8bb1804d8a92814a0b6670c9)
@Antoine Labelle could you please update the library overview and undergrad

math list to reflect recent progress in representation theory?
**[feat(*): define classes for coercions that are

homomorphisms](https://github.com/leanprover-
community/mathlib/commit/6965ed89a67095feb8379e8eee64e3c2444f7538)**
(mathlib#17048)
This PR is part of my plan to refactor algebra_map. It introduces new
classes that should connect coercions (↑s) and bundled homomorphisms, e.g.
ring_hom, so that e.g. an instance of coe_ring_hom R S states that there
is a canonical ring homomorphism ring_hom.coe R S from R to S. These
classes are unbundled (they take an instance of has_lift_t R S as a
parameter, rather than extending has_lift_t or one of its subclasses) for
two reasons:

We wouldn't have to introduce new classes that handle transitivity (and probably cause diamonds)
It doesn't matter whether a coercion is written with has_coe or has_lift, you can give it a homomorphism structure in exactly the same way.

Additions


classes coe_add_hom M N, coe_mul_hom, coe_one_hom, coe_zero_hom state that the coercion map coe : M → N preserves the corresponding operation. They take in a has_lift_t instance so it doesn't matter how precisely the coercion map is defined as long as Lean can find the instance.
classes coe_monoid_hom M N, coe_add_monoid_hom M N, coe_monoid_with_zero_hom M N, coe_non_unital_ring_hom R S and coe_ring_hom R S are convenient groupings of the above classes
simp lemmas coe_add, coe_mul, coe_zero, coe_one: basic lemmas stating that coe preserves the corresponding operation.
simp lemmas coe_pow, coe_nsmul, coe_zpow, coe_zsmul, coe_bit0, coe_bit1, coe_sub, coe_neg: lemmas stating coe preseves the derived structure
simp lemmas coe_inv, coe_div (for groups), coe_inv₀, coe_div₀ (for groups with zero). An alternative to having this pair of otherwise identical lemmas would be to add coe_inv_hom and coe_div_hom classes.
class coe_smul_hom M X Y stating that coe : X → Y preseves scalar multiplication by elements of M
class coe_semilinear_map σ M N stating that coe : M → N is σ-semilinear. coe_linear_map R M N is a synonym of coe_semilinear_map (ring_hom.id R) M N and also gives an instance of coe_smul_hom. I don't think this has any applications yet, it was mostly to test that this design would also work for more complicated classes.
definitions mul_hom.coe, add_hom.coe, one_hom.coe, zero_hom.coe, monoid_hom.coe, add_monoid_hom.coe, monoid_with_zero_hom.coe, non_unital_ring_hom.coe, ring_hom.coe, semilinear_map.coe and linear_map.coe, given the appropriate coe_hom class, are bundled forms of the coercion map that correspond to the coe_hom classes. In particular ring_hom.coe should become an alternative to algebra_map.
mul_action_hom.coe, distrib_mul_action_hom.coe and mul_semiring_action_hom.coe are bundled forms of the coercion map corresponding to coe_smul_hom (since they only vary in hypotheses on the non-bundled structure)

Changes

Whenever existing lemmas had a name conflict with the new generic coe_
lemmas, I have made them protected. In many places, the new lemmas are
silently used instead of the now protected old lemmas. This caused the vast
majority of changed lines. The full list is:

add_monoid_hom.coe_mul (is about coe_fn)
linear_map.coe_one and linear_map.coe_mul (are about coe_fn and endomorphisms)
submodule.coe_zero, submodule.coe_add, submodule.coe_smul (superseded)
dfinsupp.coe_zero, dfinsupp.coe_add, dfinsupp.coe_nsmul, dfinsupp.coe_neg, dfinsupp.coe_sub, dfinsupp.coe_zsmul, dfinsupp.coe_smul (are about coe_fn)
finset.coe_one (superseded)
finsupp.coe_smul, finsupp.coe_zero, finsupp.coe_add, finsupp.coe_neg, finsupp.coe_sub, finsupp.coe_mul (are about coe_fn)
enat.coe_zero, enat.coe_one, enat.coe_add, enat.coe_sub, enat.coe_mul (superseded except coe_sub)
nnrat.coe_zero, nnrat.coe_one, nnrat.coe_add, nnrat.coe_mul, nnrat.coe_inv, nnrat.coe_div, nnrat.coe_bit0, nnrat.coe_bit1, nnrat.coe_sub (superseded except coe_sub)
ereal.coe_zero, ereal.coe_one, ereal.coe_add, ereal.coe_mul, ereal.coe_nsmul, ereal.coe_pow, ereal.coe_bit0, ereal.coe_bit1 (superseded)
ennreal.coe_zero, ennreal.coe_one, ennreal.coe_add, ennreal.coe_mul, ennreal.coe_bit0, ennreal.coe_bit1, ennreal.coe_pow, ennreal.coe_inv, ennreal.coe_div (superseded)
equiv.perm.coe_one and equiv.perm.coe_mul (are about coe_fn and endomorphisms)
submonoid.coe_one, submonoid.coe_mul, submonoid.coe_pow (superseded)
subsemigroup.coe_mul (superseded)
special_linear_group.coe_inv, special_linear_group.coe_mul, special_linear_group.coe_pow
vector_measure.coe_smul, vector_measure.coe_zero, vector_measure.coe_add, vector_measure.coe_neg (are about coe_fn)
lucas_lehmer.X.coe_mul (superseded)
power_series.coe_add, power_series.coe_zero, power_series.coe_mul, power_series.coe_one, power_series.coe_bit0, power_series.coe_bit1, power_series.coe_pow (superseded)
uniform_space.completion.coe_zero, uniform_space.completion.coe_neg, uniform_space.completion.coe_sub, uniform_space.completion.coe_add (superseded)
continuous_function.coe_mul, continuous_function.coe_one, continuous_function.coe_inv, continuous_function.coe_div continuous_function.coe_pow, continuous_function.coe_zpow (are about `coe_fn)
bounded_continuous_function.coe_zero, bounded_continuous_function.coe_one, bounded_continuous_function.coe_add, bounded_continuous_function.coe_neg, bounded_continuous_function.coe_sub, bounded_continuous_function.coe_mul, bounded_continuous_function.coe_nsmul, bounded_continuous_function.coe_zsmul, bounded_continuous_function.coe_pow,

Many coe_ or cast_ lemmas have been reimplemented using coe_hom classes
and are no longer @[simp]. Many homomorphisms subfoo.subtype have been
reimplemented by foo_hom.coe. We might consider replacing all of these
outright.
Finally, some simp calls had to be fixed, e.g. simp [← something.cast_add]
could loop due to the new coe_add lemma, so it had to become simp [← something.cast_add, -coe_add].
Further plans

Some obvious further steps that I didn't feel fit in the (already wide) scope
of this PR:

Reviewing for missing instances: currently I only added the obvious instances for the new classes, so we should go through and ensure everything has its instance.
Reviewing for missing coe lemmas: currently I only added lemmas that existed in the submonoid/subgroup/subring files, so we should go through and ensure everything has its lemma.
Instances for the transitivity instances coe_trans and lift_trans, so if coe : M → N is a monoid hom and coe : N → O is a monoid hom then coe : M → O is also a monoid hom.
Classes for when coe_fn is a homomorphism: many of the naming conflicts that required protected are of the form mul_hom.coe_mul : ⇑(f * g) = ⇑f * ⇑g, so the obvious consequence is adding a class coe_fn_mul_hom along these same lines as in this PR.
Combining with the algebra.to_has_lift_t instance: this is likely to require some subtle fixing so I'd rather merge the big changes first so I don't have to keep those up to date as well.

Co-authored-by: Anne Baanen <t.baanen@vu.nl>
Authored-by: Vierkantor
[(commit)](https://github.com/leanprover-
community/mathlib/commit/6965ed89a67095feb8379e8eee64e3c2444f7538)
**[fix timeouts](https://github.com/leanprover-

community/mathlib/commit/933620c02ed75edc03b4f78a937079a97e80dbe2)**
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/933620c02ed75edc03b4f78a937079a97e80dbe2)
**[Revert "fix timeouts"](https://github.com/leanprover-

community/mathlib/commit/23cd34bb72a981cedba18f4ba28e920ef4097e9e)**
This reverts commit 933620c02ed75edc03b4f78a937079a97e80dbe2.
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/23cd34bb72a981cedba18f4ba28e920ef4097e9e)
**[feat(tactic/move_add, test/move_add): a tactic for moving around

summands](https://github.com/leanprover-
community/mathlib/commit/e8b1a29393c448c15e4cfeef8404cbde0b9cfa68)**
(mathlib#13483)
This PR introduces a tactic for moving summands of an expression. Individual
terms can be named, also using pattern-matching, and moved to the beginning or
to the end of the sum.
#14228 shows a
sample of golfing and usage of move_add, and the
[diff](https://github.com/leanprover-
community/mathlib/compare/aa_sort...adomani_move_add_random_golf) between
them.
#14618 contains
the doc-string update to ac_change: I moved it to a separate PR to save CI
cycles.
See compute_degree in [#14040](https://github.com/leanprover-
community/mathlib/pull/14040) for a related tactic to compute degrees and
nat_degrees of polynomials that uses move_add.
A future PR may add support for sorting also factors of a product, though
this may happen after the switch to Lean4.
Co-authored-by: Arthur Paulino
<arthurleonardo.ap@gmail.com>
Authored-by: adomani
[(commit)](https://github.com/leanprover-
community/mathlib/commit/e8b1a29393c448c15e4cfeef8404cbde0b9cfa68)
**[chore(ring_theory):

splitring_theory.algebra_tower](https://github.com/leanprover-
community/mathlib/commit/f4bce070e199b891da8bcde576326bdf9ab3129c)**
(mathlib#17480)
Remove the dependency of the file ring_theory.algebra_tower on
ring_theory.adjoin.fg by moving all those results to a new file
ring_theory.adjoin.tower, because that dependency carries with it a large
amount of imports from mv_polynomial.
In a follow-up PR I want to adjust ring_theory.finiteness so we don't need
to import mv_polynomial there either, with the eventual goal that our
definition of finite dimensional vector space doesn't import mv_polynomial.
Authored-by: Vierkantor
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f4bce070e199b891da8bcde576326bdf9ab3129c)
**[feat(topology/sheaves): Locally surjective maps of

presheaves](https://github.com/leanprover-
community/mathlib/commit/fb7698eb37544cbb66292b68b40e54d001f8d1a9)**
(mathlib#15398)
For presheaves valued in a concrete category, we define locally surjective
maps of presheaves and show that this condition is equivalent to all the
induced maps of stalks being surjective.
We also introduce notation for the types of sections, germs and corresponding
induced maps.
Co-authored by: Sam van Gool @samvang
Co-authored-by: erd1 <the.erd.one@gmail.com>

Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com
Authored-by: jakelev
[(commit)](https://github.com/leanprover-
community/mathlib/commit/fb7698eb37544cbb66292b68b40e54d001f8d1a9)
**[feat(tactic/positivity): Extension for natural powers in

acanonically_ordered_comm_semiring](https://github.com/leanprover-
community/mathlib/commit/1158f6d88df46d30c657ffce6bfdb9e9aceb4955)**
(mathlib#17535)
Provide positivity_canon_pow, a positivity extension for a ^ n where a
is in a canonically_ordered_comm_semiring. Typically, this applies to
ennreal, which is not covered by the existing positivity_pow extension.
Authored-by: YaelDillies
[(commit)](https://github.com/leanprover-
community/mathlib/commit/1158f6d88df46d30c657ffce6bfdb9e9aceb4955)
**[refactor(topology/{fiber,vector}_bundle): makevector_bundle a

mixin](https://github.com/leanprover-
community/mathlib/commit/b8c810e2aac4a30bf8cda1e1c38d4f2e6065b2e7)**
(mathlib#17505)
Previously, is_fiber_bundle* was a propositional typeclass on a function p : Z → B, stating the existence of local trivializations covering Z. Then
vector_bundle* was a class with data on a type E : X → Type* (with the
projection from Σ x : B, E x to B playing the role of p), giving a fixed
atlas of fibrewise-linear local trivializations.
We change this definition so that

(i) the data is all held in fiber_bundle, with vector_bundle a mixin
stating fibrewise-linearity

(ii) only sigma-types can be fiber bundles, not general topological spaces
This allows bundles to carry instances of typeclasses in which the scalar
field, R, does not appear as a parameter. Notably, we would like a vector
bundle over R with fibre F over base B to be a charted_space (B × F),
with the trivializations providing the charts. This would be a dangerous
instance for typeclass inference, because R does not appear as a parameter
in charted_space (B × F). But if the data of the trivializations is held in
fiber_bundle, then a fibre bundle with fibre F over base B can be a
charted_space (B × F), and this is safe for typeclass inference.
We expect that this refector will also streamline constructions of fibre
bundles with similar underlying structure (e.g., the same bundle being both a
real and complex vector bundle).
Here is the relevant Zulip discussion.
*We take the opportunity to rename topological_{fiber,vector}_bundle to {fiber,vector}_bundle, since in the upcoming definition of smooth bundles, smoothness will be another mixin for fiber_bundle.
Co-authored-by: Floris van Doorn
fpvdoorn@gmail.com
Authored-by: hrmacbeth
[(commit)](https://github.com/leanprover-
community/mathlib/commit/b8c810e2aac4a30bf8cda1e1c38d4f2e6065b2e7)
**[fix(tactic/linarith): fix bug in linarith](https://github.com/leanprover-

community/mathlib/commit/693ae04fbc9cfe7fe0be4b0eb83ab3ee3b4268da)**
(mathlib#17307)
I discovered this bug while porting linarith to mathlib4, and @digama0
minimised and identified the problem. There is a zulip discussion explaining
the details.
When applying Imbert's first acceleration
theorem
the code was incorrectly interpreting what an "implicitly eliminated variable"
was.
I've added two tests, a one-liner that Mario reduced the problem too, as well
as a longer one which had been failing in the mathlib4 port (due to different
variable ordering).
The change causes one proof to timeout, which has been sped up.
Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>

Co-authored-by: Eric Wieser
<wieser.eric@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/693ae04fbc9cfe7fe0be4b0eb83ab3ee3b4268da)
**[refactor(*): scrub imports](https://github.com/leanprover-

community/mathlib/commit/70fd9563a21e7b963887c9360bd29b2393e6225a)**
(mathlib#17568)
For each file, we read each declaration and find the files containing each
referenced declaration. This is the "needed" set. We then replace the imports
with

imports which are needed
other needed files which would not otherwise be transitively imported

Thus we don't remove any imports merely because they are transitively
redundant. Instead we remove imports only if they are genuinely unnecessary.
We also have to add back in imports (because they have been removed from
higher up the import hierarchy).
I've committed the Lean script (thanks Mario!) that generates the underlying
data, but not the Mathematica notebook that does that import calculations and
text replacement (because it's a mess, and I want this merged quickly before
it rots).

We try not to reorder imports unnecessarily.
But we don't sort: anything new that needs to be added just comes after the existing imports.
This drops a few comments on import lines.
It replaces a few import X with import X.default. (I think this is not bad: we probably want to remove all the .default files anyway at some point.)

Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/70fd9563a21e7b963887c9360bd29b2393e6225a)
**[refactor(analysis): change the symbol for norm to align with the unicode

spec](https://github.com/leanprover-
community/mathlib/commit/17ef379e997badd73e5eabb4d38f11919ab3c4b3)**
(mathlib#17575)
The characters in question are:

U+2016 DOUBLE VERTICAL LINE ‖. The Unicode Character Database says "used in pairs to indicate norm of a matrix", for instance here and here
U+2225 PARALLEL TO ∥. On some platforms this renders with a forward slant!

Previously norm was the latter and parallel was the former. This change
swaps them around:

∥x∥, S ‖ T: before
‖x‖, S ∥ T: after

Code using U+2016 ‖ for fintype cardinality has been left unchanged.
Authored-by: eric-wieser
[(commit)](https://github.com/leanprover-
community/mathlib/commit/17ef379e997badd73e5eabb4d38f11919ab3c4b3)
**[feat(measure_theory/integral): substitution without continuity at

endpoints](https://github.com/leanprover-
community/mathlib/commit/0d4bacdc2930783dc32be32943331a38276d60cd)**
(mathlib#17540)
This PR generalises the substitution law ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u to remove the assumption that g be continuous at the
endpoints of the interval. (A subsequent PR will use this to prove that
Γ(1/2) = sqrt(π).)
Authored-by: loefflerd
[(commit)](https://github.com/leanprover-
community/mathlib/commit/0d4bacdc2930783dc32be32943331a38276d60cd)
rss-bot said:


[feat(*): bump to lean 3.49.1](https://github.com/leanprover-
community/mathlib/commit/39af7d3bf61a98e928812dbc3e16f4ea8b795ca3)
([mathlib#17609](https://github.com/leanprover-
community/mathlib/pull/17609))
Authored-by: gebner
[(commit)](https://github.com/leanprover-
community/mathlib/commit/39af7d3bf61a98e928812dbc3e16f4ea8b795ca3)

This release means that the integral symbol in
[docs#circle_integral.integral_smul](https://leanprover-
community.github.io/mathlib_docs/find/circle_integral.integral_smul) is now
clickable in the web docs
**[feat(combinatorics/young): add equivalence between Young diagrams and lists

of natural numbers](https://github.com/leanprover-
community/mathlib/commit/a22eb8a834ff77be21ed3f31cbcc2ab3a5df0496)**
(mathlib#17445)
Construct the equivalence between Young diagrams and weakly decreasing lists
of positive natural numbers:

equiv_list_row_lens : young_diagram ≃ {w : list ℕ // w.sorted (≥) ∧ ∀ x ∈ w, 0 < x}
Co-authored-by: Kyle Miller
<kmill31415@gmail.com>
Authored-by: jakelev
[(commit)](https://github.com/leanprover-
community/mathlib/commit/a22eb8a834ff77be21ed3f31cbcc2ab3a5df0496)
**[feat(topology/uniform_space/uniform_convergence): more locally uniform

limit API](https://github.com/leanprover-
community/mathlib/commit/18b61ef3241e0ca361f1c976aae902b7593d6caf)**
(mathlib#17092)
Add more API around tendsto_locally_uniformly_on, needed for
#17074.
Authored-by: vbeffara
[(commit)](https://github.com/leanprover-
community/mathlib/commit/18b61ef3241e0ca361f1c976aae902b7593d6caf)
**[feat(analysis/normed/group/add_circle): results about finite-order points

on the circle](https://github.com/leanprover-
community/mathlib/commit/084f76e20c88eae536222583331abd9468b08e1c)**
(mathlib#17321)
The main motivation for developing this API is the lemma
add_circle.le_add_order_smul_norm_of_is_of_fin_add_order
Co-authored-by: Eric Wieser
<wieser.eric@gmail.com>
Authored-by: ocfnash
[(commit)](https://github.com/leanprover-
community/mathlib/commit/084f76e20c88eae536222583331abd9468b08e1c)
**[feat(analysis/calculus): smoothness of series of

functions](https://github.com/leanprover-
community/mathlib/commit/563bbc0c4bb418d36022c9c0ee4917d4f1bec7fc)**
(mathlib#17110)
We show that infinite series of functions are continuous/differentiable/smooth
under suitable summability assumptions.
Authored-by: sgouezel
[(commit)](https://github.com/leanprover-
community/mathlib/commit/563bbc0c4bb418d36022c9c0ee4917d4f1bec7fc)
**[feat(geometry/euclidean/angle/sphere): affine circle

theorems](https://github.com/leanprover-
community/mathlib/commit/8d9836ff2f455917386e28a31f86af07b3d56364)**
(mathlib#17279)
Add (oriented) Euclidean affine space versions of "angle at center of a circle
equals twice angle at circumference" and "angles in same segment are equal" /
"opposite angles of a cyclic quadrilateral add to π" (which were previously
only present for angles between vectors, not for angles between points in an
oriented Euclidean affine space).
Authored-by: jsm28
[(commit)](https://github.com/leanprover-
community/mathlib/commit/8d9836ff2f455917386e28a31f86af07b3d56364)
**[feat (analysis/fourier): Fourier analysis on the additive

circle](https://github.com/leanprover-
community/mathlib/commit/7922df8f9263a42f1b1a502a0f0991d7a0bd330b)**
(mathlib#17598)
This ticket rewrites the existing analysis.fourier file to base things on
the additive circle add_circle T = ℝ / ℤ • T rather than the unit circle in
ℂ as before. This makes it much easier to actually evaluate Fourier
coefficients, because we can link up with the huge library of lemmas about
integration on subsets of ℝ.
I've tried to keep the main part of Heather's code much as it was before; I
did refactor one lemma about conjugation-invariant subalgebras of C(X, ℂ),
moving the bulk of it into stone_weierstrass.
Authored-by: loefflerd
[(commit)](https://github.com/leanprover-
community/mathlib/commit/7922df8f9263a42f1b1a502a0f0991d7a0bd330b)
**[chore(*): add mathlib4 synchronization

comments](https://github.com/leanprover-
community/mathlib/commit/cb1d2791ea461923a4106140e5f9c684a84fea22)**
(mathlib#17686)
Regenerated from the [port status wiki page](https://github.com/leanprover-
community/mathlib/wiki/mathlib4-port-status).

Relates to the following PRs:

algebra.char_zero.defs: leanprover-community/mathlib4#661
algebra.group.inj_surj: leanprover-community/mathlib4#707
algebra.group.order_synonym: leanprover-community/mathlib4#651
algebra.group.units: leanprover-community/mathlib4#549
algebra.hierarchy_design: leanprover-community/mathlib4#657
algebra.opposites: leanprover-community/mathlib4#644
algebra.quotient: leanprover-community/mathlib4#643
algebra.ring.defs: leanprover-community/mathlib4#655
algebra.ring.order_synonym: leanprover-community/mathlib4#671
control.equiv_functor: leanprover-community/mathlib4#649
data.dlist.basic: leanprover-community/mathlib4#616
data.int.cast.basic: leanprover-community/mathlib4#670
data.lazy_list: leanprover-community/mathlib4#686
data.list.lex: leanprover-community/mathlib4#672
data.option.n_ary: leanprover-community/mathlib4#656
data.sigma.lex: leanprover-community/mathlib4#646
data.ulift: leanprover-community/mathlib4#703
group_theory.eckmann_hilton: leanprover-community/mathlib4#626
logic.equiv.basic: leanprover-community/mathlib4#631
order.iterate: leanprover-community/mathlib4#648

Authored-by: [leanprover-community-bot](https://github.com/leanprover-
community-bot) [(commit)](https://github.com/leanprover-
community/mathlib/commit/cb1d2791ea461923a4106140e5f9c684a84fea22)
**[feat(special_functions/gaussian): compute

Gamma(1/2)](https://github.com/leanprover-
community/mathlib/commit/f17ed406bd40ab3293b1ba2ae763ab19e5184f75)**
(mathlib#17543)
Uses the Gaussian-integral computation, together with some results on
integration by substitution from [#17542](https://github.com/leanprover-
community/mathlib/pull/17542), to evaluate Gamma (1 / 2) = sqrt real.pi.

 depends on: #17540
 depends on: #17542

Authored-by: loefflerd
[(commit)](https://github.com/leanprover-
community/mathlib/commit/f17ed406bd40ab3293b1ba2ae763ab19e5184f75)
**[chore(*): add mathlib4 synchronization

comments](https://github.com/leanprover-
community/mathlib/commit/1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a)**
(mathlib#17736)
Regenerated from the [port status wiki page](https://github.com/leanprover-
community/mathlib/wiki/mathlib4-port-status).

Relates to the following PRs:

algebra.group.semiconj: leanprover-community/mathlib4#717
algebra.group_with_zero.basic: leanprover-community/mathlib4#669
algebra.group_with_zero.inj_surj: leanprover-community/mathlib4#722
algebra.ring.inj_surj: leanprover-community/mathlib4#734
algebra.ring.units: leanprover-community/mathlib4#746
data.finite.defs: leanprover-community/mathlib4#698
order.lattice: leanprover-community/mathlib4#642

Authored-by: [leanprover-community-bot](https://github.com/leanprover-
community-bot) [(commit)](https://github.com/leanprover-
community/mathlib/commit/1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a)
**[feat(algebra/module/composition_series): Jordan-Hölder for

modules](https://github.com/leanprover-
community/mathlib/commit/cce7f68a7eaadadf74c82bbac20721cdc03a1cc1)**
(mathlib#17295)
Co-authored-by: D.M.H. van Gent
<gentdmhvan@u0031838.vuw.leidenuniv.nl>

Co-authored-by: Yaël Dillies
<yael.dillies@gmail.com>
Authored-by: MadPidgeon
[(commit)](https://github.com/leanprover-
community/mathlib/commit/cce7f68a7eaadadf74c82bbac20721cdc03a1cc1)
**[chore(*): revert #17048](https://github.com/leanprover-

community/mathlib/commit/a148d797a1094ab554ad4183a4ad6f130358ef64)**
(mathlib#17733)
This had merge conflicts which I've been rather reckless about resolving.
Let's see what CI says.
Co-authored-by: Scott Morrison
<scott.morrison@gmail.com>

Co-authored-by: Jireh Loreaux
<loreaujy@gmail.com>
Authored-by: semorrison
[(commit)](https://github.com/leanprover-
community/mathlib/commit/a148d797a1094ab554ad4183a4ad6f130358ef64)
**[feat(algebraic_geometry): Qcqs lemma](https://github.com/leanprover-

community/mathlib/commit/94625350b4a3482f6972f20ca146fdb0ff45e421)**
(mathlib#15996)
Co-authored-by: Andrew Yang 36414270+erdOne@users.noreply.github.com

Co-authored-by: Joël Riou <joel.riou@universite-paris-
saclay.fr>
Authored-by: erdOne
[(commit)](https://github.com/leanprover-
community/mathlib/commit/94625350b4a3482f6972f20ca146fdb0ff45e421)
**[feat(algebraic_topology/dold_kan): starting the definition of the inverse

functor of the Dold-Kan equivalence](https://github.com/leanprover-
community/mathlib/commit/369b22a4d45654180ca4397b25f3d061501a83a1)**
(mathlib#17551)
Authored-by: joelriou
[(commit)](https://github.com/leanprover-
community/mathlib/commit/369b22a4d45654180ca4397b25f3d061501a83a1)