Skip to content

Instantly share code, notes, and snippets.

@alexjbest

alexjbest/lastmsgs.md

Last active December 1, 2022 14:54
Show Gist options
  • Save alexjbest/9165fe121f57008cb93e0384209a415c to your computer and use it in GitHub Desktop.
Save alexjbest/9165fe121f57008cb93e0384209a415c to your computer and use it in GitHub Desktop.
Download ZIP
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 <[email protected]>

Authored-by: [email protected] [(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 <[email protected]>
Co-authored-by: Jon Eugster <[email protected]>

Authored-by: [email protected] [(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 [email protected]

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Joël Riou <joel.riou@universite-paris- saclay.fr>
Co-authored-by: Junyan Xu <[email protected]>

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 [email protected]

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 <[email protected]>

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 [email protected]

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 [email protected]

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 [email protected]

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.

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 <[email protected]>
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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 [email protected]

Authored-by: [email protected] [(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 <[email protected]>
Co-authored-by: Andrew Yang [email protected]

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 [email protected]

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 [email protected]

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 <[email protected]>
Co-authored-by: Junyan Xu <[email protected]>
Co-authored-by: Junyan Xu <[email protected]>

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.

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 [email protected]
Co-authored-by: Floris van Doorn <[email protected]>

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 <[email protected]>

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 <[email protected]>
Co-authored-by: RemyDegenne <[email protected]>
Co-authored-by: Kexing Ying <[email protected]>

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 [email protected]

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 <[email protected]>

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

with imports fixed up to accommodate all the overlapping changes to imports.

Co-authored-by: Yury G. Kudryashov <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>

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 <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>

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 [email protected]

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>
Co-authored-by: Andrew Yang [email protected]

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 [email protected]

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 <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

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:

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.

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:

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 <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>

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 <[email protected]>
Co-authored-by: Jireh Loreaux <[email protected]>

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 [email protected]
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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment