This makes sure that the by far most common way of declaring TODOs in module doc comments is also used by the few that deviated from that. This makes sure that it is easier to find those.

Drive by: fix number of `#` for some other headings, to make doc strings more uniform.



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

…14419)

and for the symmetric case.

…s` (#14589)

Aesthetic preference, feel free to close if this doesn't make sense.




Co-authored-by: L Lllvvuu <git@llllvvuu.dev>

Also add `MeasureTheory.Lp.simpleFunc.dense`

This matches the approach used by `Multiset`

…arly disjoint of submodules (#12434)

This is part 1 of #9651.

We adapt the definitions in <https://en.wikipedia.org/wiki/Linearly_disjoint>.
Let `R` be a commutative ring, `S` be an `R`-algebra (not necessarily commutative).
Two `R`-submodules `M` and `N` in `S` are linearly disjoint,
if the natural `R`-linear map `M ⊗[R] N →ₗ[R] S` (`Submodule.mulMap M N`)
induced by the multiplication in `S` is injective.

The following is the first equivalent characterization of linearly disjointness:

- `Submodule.LinearDisjoint.linearIndependent_left_of_flat`:
  if `M` and `N` are linearly disjoint, if `N` is a flat `R`-module, then for any family of
  `R`-linearly independent elements `{ m_i }` of `M`, they are also `N`-linearly independent,
  in the sense that the `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }`
  to the sum of `m_i * n_i` (`Submodule.mulLeftMap N m`) is injective.

- `Submodule.LinearDisjoint.of_basis_left`:
  conversely, if `{ m_i }` is an `R`-basis of `M`, which is also `N`-linearly independent,
  then `M` and `N` are linearly disjoint.

Dually, we have:

- `Submodule.LinearDisjoint.linearIndependent_right_of_flat`:
  if `M` and `N` are linearly disjoint, if `M` is a flat `R`-module, then for any family of
  `R`-linearly independent elements `{ n_i }` of `N`, they are also `M`-linearly independent,
  in the sense that the `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }`
  to the sum of `m_i * n_i` (`Submodule.mulRightMap M n`) is injective.

- `Submodule.LinearDisjoint.of_basis_right`:
  conversely, if `{ n_i }` is an `R`-basis of `N`, which is also `M`-linearly independent,
  then `M` and `N` are linearly disjoint.

The following is the second equivalent characterization of linearly disjointness:

- `Submodule.LinearDisjoint.linearIndependent_mul_of_flat`:
  if `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then for any family of
  `R`-linearly independent elements `{ m_i }` of `M`, and any family of
  `R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
  also `R`-linearly independent.

- `Submodule.LinearDisjoint.of_basis_mul`:
  conversely, if `{ m_i }` is an `R`-basis of `M`, if `{ n_i }` is an `R`-basis of `N`,
  such that the family `{ m_i * n_j }` in `S` is `R`-linearly independent,
  then `M` and `N` are linearly disjoint.

Other results:

- `Submodule.LinearDisjoint.symm_of_commute`, `Submodule.linearDisjoint_symm_of_commute`:
  linearly disjoint is symmetric under some commutative conditions.

- `Submodule.linearDisjoint_op`:
  linearly disjoint is preserved by taking multiplicative opposite.

- `Submodule.LinearDisjoint.of_le_left_of_flat`, `Submodule.LinearDisjoint.of_le_right_of_flat`,
  `Submodule.LinearDisjoint.of_le_of_flat_left`, `Submodule.LinearDisjoint.of_le_of_flat_right`:
  linearly disjoint is preserved by taking submodules under some flatness conditions.

- `Submodule.LinearDisjoint.of_linearDisjoint_fg_left`,
  `Submodule.LinearDisjoint.of_linearDisjoint_fg_right`,
  `Submodule.LinearDisjoint.of_linearDisjoint_fg`:
  conversely, if any finitely generated submodules of `M` and `N` are linearly disjoint,
  then `M` and `N` themselves are linearly disjoint.

- `Submodule.LinearDisjoint.bot_left`, `Submodule.LinearDisjoint.bot_right`:
  the zero module is linearly disjoint with any other submodules.

- `Submodule.LinearDisjoint.one_left`, `Submodule.LinearDisjoint.one_right`:
  the image of `R` in `S` is linearly disjoint with any other submodules.

- `Submodule.LinearDisjoint.of_left_le_one_of_flat`,
  `Submodule.LinearDisjoint.of_right_le_one_of_flat`:
  if a submodule is contained in the image of `R` in `S`, then it is linearly disjoint with
  any other submodules, under some flatness conditions.

- `Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat`,
  `Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat`:
  if `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then any two commutative
  elements contained in the intersection of `M` and `N` are not `R`-linearly independent (namely,
  their span is not `R ^ 2`). In particular, if any two elements in the intersection of `M` and `N`
  are commutative, then the rank of the intersection of `M` and `N` is at most one.

- `Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self`:
  if `M` and itself are linearly disjoint, if `M` is flat, if any two elements in `M`
  are commutative, then the rank of `M` is at most one.

The results with name containing "of_commute" also have corresponding specified versions
assuming `S` is commutative.

Its implementation has been improved in `lean4lean` and `batteries`; the mathlib implementation can be removed in favour of these.

Searching github for 'import Mathlib.Data.UnionFind' only yields forks of mathlib (either explicit or manual); hence this seems safe to remove without a deprecation period.

Fixes two typos in `Data/Nat/Nth.lean`.

leanprover/lean4#1866 is merged, so this can go.



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

This PR updates the Mathlib dependencies.

If two diagrams involving additive maps are isomorphic, one is exact (in the sense of `Function.Exact`) iff the other is. In this PR, we also relate `Function.Exact` and `ShortComplex.Exact` in the categories of abelian groups and modules over a ring.



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

A strongly atomic preorder is one in which every nontrivial interval `[a,b]` contains an element covering `a`, or equivalently an order where every closed interval is atomic. We add a new typeclass `IsStronglyAtomic` to capture this.

We provide instances of this typeclass for `SuccOrder`s, orders with `WellFoundedLT`, atomistic upper-modular lattices, complemented atomic modular lattices, and `OrdConnected` subtypes. We also show that such orders are atomic.

We also provide the dual typeclass `IsStronglyCoatomic` and dual versions of all of the above.

…13034)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

…les (#13478)

This PR characterises epimorphisms in condensed sets and condensed `R`-modules for any ring `R`, as morphisms of sheaves which are objectwise surjective on `Stonean`. 



Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>

Shows that the forgetful functor `forget T : Coalgebra T ⥤ C` for a comonad `T : C ⥤ C` creates colimits and creates any limits which `T` preserves. This is used to show that `Coalgebra T` has any colimits which `C` has, and any limits which `C` has and `T` preserves. This is generalised to the case of a comonadic functor `D ⥤ C`.

Dualises everything currently in [Mathlib.CategoryTheory.Monad.Limits](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Limits.html).

This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.



Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>

…der`. (#14616)

Adds a `CompleteLinearOrder` instance for `[NeZero n] Fin n`.

Maybe, `applyc` in lean3 also tried `assumption`, so I added it here!

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/isBoundedDefault.20not.20triggering)

The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more direct way: using pasting composition on 2-cells. 

This pull request:
(i) proposes a new definition of `Mates` to replace and rename the existing `transferNatTrans`
(ii) proposes a new definition of `Conjugates` to replace and rename the existing `transferNatTransSelf`
(iii) proves that the mates correspondence commutes with horizontal and vertical composition of squares, as well as some coherences relating mates to conjugates
(iv) updates the files that depends on this, involving two new proofs about exponentiation in cartesian closed categories

…#14559)

These are redundant. Unfortunately there's two cases involving `GradedAlgebra` where a direct replacement times out, so I ignored those for now.

…14621)

Automatically generated from the linter in #14378.
#14620 contains a few manual tweaks; these PRs can be landed in any order (and the second one rebased on the first).



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

…4615)

As discussed at the maintainers meeting. This more accurately reflects their position, in that they are not expected to remain involved in maintainer discussions.

As explained by the module doc, we are missing the `Fin.succAbove` equivalent of `Fin.tail`/`Fin.init`. In fact, it already exists as the second projection of `extractNth`, so this PR deletes `extractNth` and defines its second projection as a new function `removeNth`.

- Topology/Separation: fix typo "section/end"
- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean: fix typo "namespace/end" In both cases, a second identical section resp. namespace was *opened* instead of closing the existing one.

- Topology/ExtremallyDisconnected: remove superfluous anonymous section. The entire file is already inside a noncomputable section; this sections adds nothing on top. (The nested section is also processed as a noncomputable section.)

- RingTheory/Bialgebra/Basic, RingTheory/HopfAlgebra: remove section CommRing in favour of the namespace CommRing a few lines later

- ModuleCat/Sheaf/Colimits: remove duplicate namespace SheafOfModules
- Probability/Distributions/Uniform.lean: this file is inside a noncomputable section already; a *second* such section (nested right under the first) was superfluous

…ment (#14663)

I checked the raw form of some comments and they were missing the `\r`, so I'm pretty sure this is why some of them get ignored by the bots.

Moving it to a new file `Analysis.Calculus.AddTorsor.Coord` significantly reduces the imports to `Analysis.NormedSpace.AddTorsorBases`. Also rename `Analysis.Calculus.AffineMap` to `Analysis.Calculus.AddTorsor.AffineMap`.

…`Algebra.Order.Group` to a different file (#14667)

Following the discussion on #14598, move `LinearOrderedAddCommMonoidWithTop`, `LinearOrderedAddCommGroupWithTop`, and associated theorems to `Algebra.Order.AddGroupWithTop`.



Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

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

.. from `T2Space` to `R1Space`

We construct the natural map `AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M` for any
`R`-module `M` and ideal `I` and show that it is an isomorphism for `M = R^n` and surjective if `M` is a finite `R`-module.

Co-authored-by: Judith Ludwig <ludwig@mathi.uni-heidelberg.de>

I may be tilting at windmills, but I've removed `@[simp]` from `List.replicate_succ` in Lean, and I think it results in slightly better simp normal forms in some situations. We don't yet have automatic post-Mathlib testing of simp normal forms, but I hope we will eventually.

In the meantime, this removes an inconsistency by cancelling Mathlib's downstream addition of `@[simp]` to `List.replicate.succ`. Mathlib doesn't mind much.

... to the preimage of an open set is a quotient map.

- [x] depends on: #13319 
- [x] depends on: #13355

…ciated to a module (#14231)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Johan Commelin <j.m.commelin@uu.nl>
Co-authored-by: Amelia Livingston <al3717@ic.ac.uk>
Co-authored-by: Sophie Morel <sophie.morel@ens-lyon.fr>
Co-authored-by: Jujian Zhang <jujian.zhang1998@gmail.com>

This PR was done during the AIM workshop Formalizing Algebraic Geometry.



Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Co-authored-by: morel <smorel@math.princeton.edu>

The density of a finite set in an ambient group is a quantity of great interest in combinatorics.
This PR defines `Finset.dens s` for `s : Finset α` as the size of `s` divided by the size of `α`, with value in any semifield.
The API lemmas are copied from `Finset.card` (but not all `Finset.card` lemmas are sensible `Finset.dens` lemmas).

From LeanAPAP

We define an extended version of the exponential from `EReal` to `ENNReal` and prove some properties in relation to the extended log.

- [x] Rename `ENNReal.lean` to `ENNRealLog.lean`
- [x] Add `ENNRealExp.lean`
- [x] Add `ENNRealLogExp.lean`

See [this](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Porting.20TopologicalEntropy.20into.20Mathlib/near/446665481) Zulip discussion.

Co-authored-by: @RemyDegenne @pitmonticone @D-Thomine 




Co-authored-by: Lorenzo Luccioli <lorenzoluccioli@gmail.com>

…rings. (#14550)

…ff_right` (#14593)

Given a function differentiable at a point, the result of adding a second function is differentiable (there) iff the second function is differentiable (there).

These were found by the linter at #14379.

Co-authored-by: Michael Rothgang <[rothgami@math.hu-berlin.de](mailto:rothgami@math.hu-berlin.de)>

This PR updates the Mathlib dependencies.

Those will be needed in a future file `Algebra.GroupWithZero.Action.Defs`

This PR updates the Mathlib dependencies.

Provide the additive action of a module `V` over the `k`-affine bases of a `V`-torsor `P`.




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

Also generalize `exists_absolutelyContinuous_isFiniteMeasure` and some downstream lemmas.

Deletions:
- MeasureTheory.Measure.restrict.instIsFiniteMeasure

…14680)