This is a specialization of the Cauchy-Schwarz inequality which is often useful in math olympiad problems.

In order to prove it in general ordered semifields, we have to show slightly more general forms of the AM-GM and Cauchy-Schwarz inequalities, which indirectly work with square roots.

Co-authored-by: Alex Brodbelt <64128135+AlexBrodbelt@users.noreply.github.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

From Kneser (LeanCamCombi)

The `Category` assumption is unused, as `Discrete` subsumes it.

…18803)

…t on residue classes (#19418)

This continues the sequence of PRs on the way to **Dirichlet's Theorem**.

This one adds some properties of the von Mangoldt function `Λ` restricted to a residue class: if further restricted to primes, its support is the set of primes in that residue class, and the function `n ↦ Λ n / n`, restriced to non-primes in a residue class, is summable (the latter will be important in deducing information on the former).

See [here](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/Prerequisites.20for.20PNT.20and.20Dirichlet's.20Thm/near/483904451) on Zulip.

This adds the key technical lemma in the proof of Mahler's theorem characterising continuous functions on Zp: for any continuous function, the iterated forward differences at 0 tend to zero.

Co-authored-by: Giulio Caflisch <gcaflisch@student.ethz.ch>

From LeanAPAP

I am happy to remove some nolints for you!

to hide the defeq abuse `f ⁻¹ᵁ ⊤ = ⊤`

I noticed that there is notation for a non-unital monoid hom but not for a non-unital additive monoid hom,
and since I'm working on extensions of non-unital homomorphisms in my PR's on quantale, I found it natural to add this.

This PR updates the Mathlib dependencies.

If the `!bench` summary contains no entry with a difference in instructions of at least 10^9, then the bot posts a message confirming this information, rather than silently failing.

The bot also posts a link to the workflow CI run that generated the message.

)

Changes the way in which emoji reactions to `delegated`, `ready-to-merge` and `merged` are applied in Zulip: instead of running periodically a script to add the reactions, the reactions are now applied at the same time that the label is applied, or when PRs are merged into master.

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Previously, the script was failing, since the script was unavailable.

…19450)

#19065)

In the current design of concrete categories in mathlib, there are two sources of `erw`s:

- Def-Eq abuse of `A ⟶ B` and `A →ₐ [R] B`: The type of `A ⟶ B` is by definition `A →ₐ[R] B`, but not at reducible transparency. So it happens that one `rw` lemma transforms a term in a form, where the next `rw` expects `A →ₐ B`. By supplying explicit `show` lines (copying the output of the pretty-printer), Lean correctly re-synthesizes the type to be `A →ₐ B` and the `rw` succeeds. This def-eq abuse hence always causes issues in the case where a lemma from the non-category theoretic part of the library should be applied. An insightful example is the following proof excerpt from current master (proof of `AlgebraCat.adj`):
```lean
import Mathlib.Algebra.Category.AlgebraCat.Basic
open CategoryTheory AlgebraCat
variable {R : Type u} [CommRing R]
set_option pp.analyze true

example : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => (FreeAlgebra.lift _).symm
      homEquiv_naturality_left_symm := by
        intro X Y Z f g
        apply FreeAlgebra.hom_ext
        ext x
        simp only [Equiv.symm_symm, Function.comp_apply, free_map]
        /- Eq (α := Z)
             (((FreeAlgebra.lift R) (f ≫ g) :
               Prefunctor.obj (Functor.toPrefunctor (free R)) X ⟶ Z) (FreeAlgebra.ι R x) : ↑Z) _
        -/
        erw [FreeAlgebra.lift_ι_apply]
        sorry
      homEquiv_naturality_right := sorry }
```
The `simp` lemma `FreeAlgebra.lift_ι_apply` expects an `AlgHom`, but as the `pp.analyze` shows, the type is synthesized as a `⟶`. With a show line before the `erw`, Lean correctly synthesizes the type as an `AlgHom` again and the `rw` succeeds. The solution is to strictly distinguish between `A ⟶ B` and `A →ₐ[R] B`: We define a new `AlgebraCat.Hom` structure with a single field `hom : A →ₐ[R] B`. The above proof is mostly solved by `ext; simp` then, except for the `ext` lemma `FreeAlgebra.hom_ext` not applying. This is because now the type is `AlgebraCat.of R (FreeAlgebra R X) →ₐ[R] _` and Lean can't see through the `AlgebraCat.of` at reducible transparency. Hence the solution is to make `AlgebraCat.of` an `abbrev`. Finally, the proof is `by ext; simp` or even `by aesop`.

- `FunLike`: An intermediate design adapted the changes from the first point, but with keeping a `FunLike` and an `AlgHomClass` instance on `A ⟶ B`. This lead to many additional `coe` lemmas for composition of morphisms, where it mattered which of the three appearing terms of `AlgebraCat` where of the form `AlgebraCat.of R A`. Eric Wieser suggested to replace the `FunLike` by a `CoeFun` which is inlined, so an invocation of `f x` turns into `f.hom x`. This has then worked very smoothly.

So the key points are:
- Homs in concrete categories should be one-field structures to maintain a strict type distinction.
- Use `CoeFun` instead of `FunLike`, since the latter is automatically inlined.
- Make `.of` constructors an `abbrev` to obtain the def-eq `↑(AlgebraCat.of R A) = A` at reducible transparency.

For more details, see the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories).

…ons between manifolds (#19296)

The abbreviation `Smooth` for `ContMDiff` with infinite smoothness had been introduced in mathlib in ancient times. This has lead to a big API duplication, for no visible gain. We deprecate this abbreviation (with its friends `SmoothAt` and so on) and all the lemmas involving it.

In the longer run, we might consider reintroducing it as a mere notation (without any specific API), but this is not part of this PR, devoted purely to the deprecation. No mathematical content added.

…pIndep`/`sSupIndep` (#19409)

These names are shorter, closer to `SupIndep` and clearer without their namespace.

From GrowthInGroups (LeanCamCombi)

…s. (#19683)

Add a comparison with the "classical" literature in the definition of a root pairing.

From FLT

Co-authored-by: Javier Lopez-Contreras <jlcontreras@gmail.com>

…19626)

…9630)

Extracted from #19634.

Adds left, right, and bi_total_empty, and golfs `identical_of_isEmpty` in `PGame` as a result.



Co-authored-by: Tristan F. <LeoDog896@hotmail.com>

…< ·)` (#18235)

The `erw` linter from #17638 caught these `erw`s that can become `rw` without breaking the proofs.

This adds `!₂[1, 2, 3]` notation for `(WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3]`, which is a term of type `EuclideanSpace 𝕜 (Fin 3)`; and more generally for other Lp norms, using the `subscript` parser.

This reduces the temptation to write the type-incorrect `![1, 2, 3]` that has the wrong norm.

The (parser for the) `subscript` parser relies on `initialize`rs running, and so a missing `Lean.enableInitializersExecution` has to be inserted in `checkYaml.lean`. It has already been inserted in the necessary places in upstream repos.

[Notation Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20for.20vectors.20in.20euclidean.20space/near/476796192).



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>

…rty of `Polynomial.hilbertPoly p d` for `p : F[X]` and `d : ℕ`, where `F` is a field. (#19303)

Given any field `F`, polynomial `p : F[X]` and natural number `d`, we have defined `Polynomial.hilbertPoly p d : F[X]`. If `F` is of characteristic zero, then for any large enough `n : ℕ`, `PowerSeries.coeff F n (p * (invOneSubPow F d))` equals `(hilbertPoly p d).eval (n : F)` (see `Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval`).

- [x] depends on: #19622 (perhaps unnecessarily)

This instance was found in `Data.Int.Cast.Lemmas` and is used quite a few times without all the theory in those files.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

…q` (#19654)

Co-authored-by: Moritz Firsching <firsching@google.com>

From GrowthInGroups (LeanCamCombi)

This PR does the following:
- remove some trivial sectioning
- explain the solution better
- remove `ProblemPredicate`, which was only used once
- replace `ring` by a short `rw` (to minimize imports)

Remove several uses of deprecated lemmas in non-deprecated lemmas.

Also convert all `set_option linter.deprecated false` to `set_option linter.deprecated false in`, so it is easier for us to count via regex what remains.

I think
```
set_option linter\.deprecated false.*(?:(?:\n/--.*?-/\n(?!.*deprecated))|\n(?!.*deprecated|/--))
```
is the correct regex to use now: it accounts properly for intervening doc-strings. It now reports that there are only ~~three~~ one! file~~s~~ that use `set_option linter.deprecated false` on non-deprecated declarations, namely:

* ~~Mathlib.Data.List.Permutation~~ (fixed by moving some List theorems earlier)
* ~~Mathlib.LinearAlgebra.CliffordAlgebra.Grading~~ (replace `AlgHom.map_zero` with just `map_zero`; only costs 2000 heartbeats)
* Mathlib.SetTheory.Ordinal.Arithmetic (which is a mess)

…#19592)

Also generalizes the instance for Finsupp.

…ove by 4 (#19343)

This PR adds a version of the Cauchy-Schwarz inequality for positive semidefinite bilinear forms on modules over linearly ordered commutative rings, and applies it to restrict Coxeter weights for root systems.



Co-authored-by: Oliver Nash <github@olivernash.org>

… module (#18389)

Given a morphism of rings `A → B` and a `B`-module `M`, we obtain a presentation of `M` as a `A`-module from a presentation of `M` as `B`-module, a presentation of `B` as a `A`-module (and some additional data).



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…eCat.ofHom` (#19705)

As discussed in the comments for #19511.

It seems the choice between `ofHom` and `asHom` is somewhat inconsistent in concrete categories, but `ofHom` wins. In particular, we want to be consistent with the newly refactored `AlgebraCat.ofHom` and the constructor for objects `ModuleCat.of`.

The choice between `asHom` and `ofHom` was only made a few months ago: #17476. It's a bit unfortunate to go back on something that was deprecated so recently, but I think the result is worth the pain.

I have not touched `asHomLeft` and `asHomRight` since #19511 will replace these with `ofHom` everywhere anyway.

…#18794)

This PR defines a pointwise product operation on summable families of Hahn series, and shows that the formal sum of the pointwise product is equal to the product of formal sums.  This is preparation for defining algebra homomorphisms from power series rings.