We derive the inequality between the harmonic and geometric mean as a consequence of AM-GM for positive real valued functions from a `Finset`. We state a weighted as well as the classical version.

This is one in a series of PRs rewriting most checks from `lint-style.py` in Lean.
This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247.

This PR also adds a `nolints` file for text-based linters.

…ance (#14050)

…es (#13545)

We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Co-authored-by: Paul Lezeau [paul.lezeau@gmail.com](mailto:paul.lezeau@gmail.com)

…14018)

This PR adds the `SpecialFunctions/Log/ENNRealLog.lean` file where we define `log` as an extension of the logarithm of a positive real to the extended nonnegative reals `ℝ≥0∞`. The function takes values in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`.

Co-authored with @D-Thomine.

left and right unitor functors for product of categories



Co-authored-by: Shanghe Chen <shanghechen@outlook.com>

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

)

If `F` is an exact functor between abelian categories, we define the induced functor on the derived categories.

We show that `Module.Finite` is preserved under localizations and that if a module is finite after localizing at a spanning set of elements of the ring, it is finite.

This reduces the long pole.

The `cc` tactic is a high-cost tactic, so I restored `cc` tactics only if a proof can be reduced significantly.
I made sure that `cc` tactic works on in the all changed proofs except when the other specification changes in Lean 4 changes a goal.



Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

- Add `slope_neg_fun`
- Add `ConvexOn.slope_mono` and `ConcaveOn.slope_anti` in a new separate section called `slope`



Co-authored-by: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

- [x] depends on: #13503

Extends `convert_to` to be able to operate on any location. When converting the type of a local hypothesis, new congruence goals come first. Suggested [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60convert_to.20at.60.20.2F.20non-definitional.20.60change.60/near/447601320).

…functor, then the unit is an isomorphism. (#14017)

This PR proves that to show that the unit of an adjunction `L ⊣ R` is an isomorphism (i.e. that L is fully faithful), it is enough to give an arbitrary isomorphism `L ⋙ R ≅ 𝟭 C`, and the dual result. 

To do this, we give a general way to transport (co)monad structures on functors along isomorphisms of functors.

…rder` (#14121)

We don't want to import the order hierarchy without really needing it.

For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$.
This can be used to prove the same property of Wronskian: see #14243.



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

We can avoid importing `Algebra.Order.Group.Defs` in `Data.Rat.Lemmas` if we use `Nat` versions of some lemmas and slightly modify one proof.

We shouldn't import the whole order hierarchy when we want ring instances on products.

We shouldn't need to import ordered algebraic classes for basic properties of pointwise multiplication of sets.

We can just specialize to the results about `Nat` and avoid importing `Algebra.Order.Ring.Nat`.

…ousOn_eval₂` (#13532)

Also use it to weaken TC assumptions in `ContinuousMultilinearMap.continuous_eval`.

Splitting `Prime.lean` into `Defs`, `Basic`. The split aims at separation of defs and needed lemmas from everything else. With this split 13/18 Mathlib modules no longer import the whole `Prime.lean`. `Prime/Defs.lean` is about half the size.

Motivation is a circular dependency that would prevent me from adding a lemma to `Prime.lean`.

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/split.20Nat.2FPrime.2Elean