diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
index 675e0867659478..5b71e302d72c81 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
@@ -16,10 +16,32 @@ public import Mathlib.Topology.Algebra.Module.Basic
 /-!
 # Continuous linear maps
 
-In this file we define continuous (semi-)linear maps, as semilinear maps between topological
-modules which are continuous. The set of continuous semilinear maps between the topological
-`R₁`-module `M` and `R₂`-module `M₂` with respect to the `RingHom` `σ` is denoted by `M →SL[σ] M₂`.
-Plain linear maps are denoted by `M →L[R] M₂` and star-linear maps by `M →L⋆[R] M₂`.
+In this file we define the type of continuous (semi)linear maps between topological
+modules that are continuous, and endow it with its algebraic structure.
+
+Later files endow it with a topological structure, see the docstring of
+`Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean`.
+
+## Main definitions
+
+* `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules that are
+  continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the
+  `σ`-semilinear case, and `M →L⋆[R] N` in the conjugate-linear (antilinear) case.
+* `StrongDual R M` is an abbreviation for `M →L[R] R`, the type of continuous `R`-linear forms on
+  `M`. As a vector space, it is often called the "topological dual of `M`". We use the name "strong
+  dual" because it will (in later files) be endowed with the strong-dual topology, namely the
+  topology of uniform convergence on bounded subsets.
+* `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : the algebraic structures
+  on `M →SL[σ] N`.
+
+## Notation
+
+* `M →L[R] N`: the type of `R`-linear continuous maps from `M` to `N`;
+* `M →SL[σ] N`: the type of `σ`-semilinear continuous maps from `M` to `N`;
+* `M →L⋆[σ] N`: the type of conjugate-linear (antilinear) continuous maps from `M` to `N`;
+* `f ∘L g`: the composition of two continuous linear maps;
+* `f ∘SL g`: the composition of two continuous semilinear maps.
+
 -/
 
 @[expose] public section
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
index cd073a5fc30887..fc0781b504f45e 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
@@ -9,6 +9,24 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
 
 /-!
 # Idempotent continuous linear maps
+
+In this file, we study the idempotent elements (`IsIdempotentElem`) of the ring `M →L[R] M` of
+continuous endomorphisms of a topological `R`-module `M`.
+
+## Main statements
+
+* `ContinuousLinearMap.isIdempotentElem_toLinearMap_iff`: `T` is idempotent as an element of
+  `M →L[R] M` if and only if it is such as an element of `M →ₗ[R] M`;
+* `ContinuousLinearMap.IsIdempotentElem.ext_iff`: idempotent elements of `M →L[R] M` are determined
+  by their range and kernel;
+* `ContinuousLinearMap.IsIdempotentElem.commute_iff`: a continuous linear map `S` commutes with
+  an idempotent `T` if and only if the range and kernel of `T` are `S`-invariant;
+* `ContinuousLinearMap.IsIdempotentElem.isCLosed_range`: an idempotent continuous linear map
+  has closed range.
+
+Further results can be found in the `Mathlib/Topology/Algebra/Module/Complement.lean` module, where
+we show that idempotent elements of `M →L[R] M` are precisely the projections associated to
+topological complement submodules.
 -/
 
 @[expose] public section
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean
index 53d34c2cfe04da..e5d262bec8c0df 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean
@@ -10,6 +10,51 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
 
 /-!
 # Continuous linear maps on products and Pi types
+
+In this file, we collect various constructions relating continuous linear maps with (binary or
+arbitrary) products.
+
+## Main definitions
+
+Binary products (viewed as categorical products):
+
+* `ContinuousLinearMap.fst R M₁ M₂ : M₁ × M₂ →L[R] M₁` and
+  `ContinuousLinearMap.snd R M₁ M₂ : M₁ × M₂ →L[R] M₂` are the two projections, given
+  respectively by `fst (x, y) = x` and `snd (x, y) = y`. These are the continuous versions
+  of `LinearMap.fst` and `LinearMap.snd`.
+* `ContinuousLinearMap.prod f₁ f₂` is the continuous linear map `M →L[R] N₁ × N₂` given by two
+  continuous linear maps `f₁ : M →L[R] N₁` and `f₂ : M →L[R] N₂`. This is the continuous version
+  of `LinearMap.prod`.
+* `ContinuousLinearMap.prodEquiv` shows that the above is a bijection: every continuous linear
+  map to a product is obtained this way. In other words, this is the universal property of the
+  product.
+* `ContinuousLinearMap.prodMap f₁ f₂` is the continuous linear map `M₁ × M₂ →L[R] N₁ × N₂` given by
+  two continuous linear maps `f₁ : M₁ →L[R] N₁` and `f₂ : M₂ →L[R] N₂`. This is the continuous
+  version of `LinearMap.prodMap`.
+
+Binary products (viewed as categorical coproducts):
+
+* `ContinuousLinearMap.inl R M₁ M₂ : M₁ →L[R] M₁ × M₂` and
+  `ContinuousLinearMap.inr R M₁ M₂ : M₂ →L[R] M₁ × M₂` are the two inclusions, given
+  respectively by `inl x = (x, 0)` and `inr x = (0, x)`. These are the continuous versions
+  of `LinearMap.inl` and `LinearMap.inr`.
+* `ContinuousLinearMap.coprod f₁ f₂` is the continuous linear map ` M₁ × M₂ →L[R] N` given by
+  two continuous linear maps `f₁ : M₁ →L[R] N` and `f₂ : M₂ →L[R] N`. This is the continuous
+  version of `LinearMap.coprod`.
+* `ContinuousLinearMap.coprodEquiv` shows that the above is a bijection: every continuous linear
+  map from a (binary) product is obtained this way. In other words, this is the universal property
+  of the coproduct.
+
+Indexed products:
+
+* `ContinuousLinearMap.pi f` is the continuous linear map `M →L[R] (Π i, N i)` given by a family
+  `f₁ : Π i, M →L[R] N i` of continuous linear maps. This is the continuous version
+  of `LinearMap.pi`.
+* `ContinuousLinearMap.piMap f` is the continuous linear map `(Π i, M i) →L[R] (Π i, N i)` given by
+  a family `f : Π i, M i →L[R] N i` of continuous linear maps. This is the continuous
+  version of `LinearMap.piMap`.
+* `ContinuousLinearMap.proj j : (Π i, M i) →L[R] M j` is the projection given by
+  `proj i f = f i`. This is the continuous version of `LinearMap.proj`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean
index c1139c3d57e565..db51786e65a5db 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean
@@ -9,6 +9,20 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
 
 /-!
 # Continuous linear maps and quotient topological modules
+
+In this file, we collect various continuous linear maps associated to quotient spaces.
+
+## Main definitions
+
+* `Submodule.mkQL S` is the quotient map `M →L[R] M ⧸ S`. In other words, it is
+  `Submodule.mkQ S` bundled as a `ContinuousLinearMap`.
+* `Submodule.liftQL S f h` is the map `M ⧸ S →SL[σ] N` given by `f : M →SL[σ] N` and a proof
+  `h : S ≤ f.ker` that `f` vanishes on `S`. In other words, it is `Submodule.liftQ S f h` bundled
+  as a `ContinuousLinearMap`.
+
+## TODO
+
+* Define `Submodule.mapQL`, the continuous linear bundling of `Submodule.mapQ`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean
index 6bddf0c74e3b03..d441ec3c01472a 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean
@@ -10,6 +10,27 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
 
 /-!
 # Restrictions of continuous linear maps to submodules
+
+In this file, we collect the various operations of restrictions of `ContinuousLinearMap`s
+to subspaces of the domain/codomain.
+
+## Main definitions
+
+* `Submodule.subtypeL S` is the inclusion map `S →L[R] M` when `S : Submodule R M`.
+  In other words, it is `Submodule.subtype S` bundled as a `ContinuousLinearMap`.
+* `ContinuousLinearMap.domRestrict f S` is the map `S →SL[σ] N` obtained by restricting
+  `f : M →SL[σ] N` to a subspace `S` of the *domain*.
+  This is the continuous version of `LinearMap.domRestrict`.
+* `ContinuousLinearMap.codRestrict f S h` is the map `M →SL[σ] S` obtained by co-restricting
+  `f : M →SL[σ] N` to a subspace `S` of the *codomain*; this requires a proof `h` that all values
+  of `f` indeed belong to `S`.
+  This is the continuous version of `LinearMap.codRestrict`.
+* `ContinuousLinearMap.rangeRestrict f` is an abbreviation for
+  `f.codRestrict f.range ⋯ : M →SL[σ] f.range`.
+  This is the continuous version of `LinearMap.rangeRestrict`.
+* `ContinuousLinearMap.restrict f h` is the map `S →SL[σ] T` obtained by restricting from
+  `f : M →SL[σ] N` and a proof `h` that `f` maps `S` inside `T`.
+  This is the continuous version of `LinearMap.restrict`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean
index b5cd37255ab4f7..7c57f0b68852a3 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean
@@ -9,6 +9,10 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
 
 /-!
 # Restriction of scalars for continuous linear maps
+
+In this file, we define and study `ContinuousLinearMap.restrictScalars`, which reinterprets
+a continuous `R`-linear map as a continuous `S`-linear map, for suitable `R` and `S`.
+This is the continuous version of `LinearMap.restrictScalars`.
 -/
 
 @[expose] public section