chore: homogenize TODO format (#14474)

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 <[email protected]>
leanprover-community · Jul 9, 2024 · ca8d01b · ca8d01b
1 parent d3f5dcd
commit ca8d01b
Show file tree

Hide file tree

Showing 58 changed files with 64 additions and 64 deletions.
diff --git a/Mathlib/Algebra/Group/NatPowAssoc.lean b/Mathlib/Algebra/Group/NatPowAssoc.lean
@@ -28,7 +28,7 @@ We also produce the following instances:
 
 - `NatPowAssoc` for Monoids, Pi types and products.
 
-## Todo
+## TODO
 
 * to_additive?
 

diff --git a/Mathlib/Algebra/Group/PNatPowAssoc.lean b/Mathlib/Algebra/Group/PNatPowAssoc.lean
@@ -27,7 +27,7 @@ powers are considered.
 
 - PNatPowAssoc for products and Pi types
 
-## Todo
+## TODO
 
 * `NatPowAssoc` for `MulOneClass` - more or less the same flow
 * It seems unlikely that anyone will want `NatSMulAssoc` and `PNatSMulAssoc` as additive versions of

diff --git a/Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean b/Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean
@@ -12,7 +12,7 @@ Given a short exact short complex `S` in an abelian category, we construct
 the associated distinguished triangle in the derived category:
 `(singleFunctor C 0).obj S.X₁ ⟶ (singleFunctor C 0).obj S.X₂ ⟶ (singleFunctor C 0).obj S.X₃ ⟶ ...`
 
-# TODO
+## TODO
 * when the canonical t-structure on the derived category is formalized, refactor
 this definition to make it a particular case of the triangle induced by a short
 exact sequence in the heart of a t-structure

diff --git a/Mathlib/Algebra/Order/Module/Algebra.lean b/Mathlib/Algebra/Order/Module/Algebra.lean
@@ -11,7 +11,7 @@ import Mathlib.Algebra.Order.Module.Defs
 
 This file proves properties of algebras where both rings are ordered compatibly.
 
-### TODO
+## TODO
 
 `positivity` extension for `algebraMap`
 -/

diff --git a/Mathlib/Algebra/Polynomial/Smeval.lean b/Mathlib/Algebra/Polynomial/Smeval.lean
@@ -30,7 +30,7 @@ is a generalization of `Algebra.Polynomial.Eval`.
 * `smeval_mul`, `smeval_comp`: multiplicativity of evaluation, given power-associativity.
 * `eval₂_eq_smeval`, `leval_eq_smeval.linearMap`, `aeval = smeval.algebraMap`, etc.: comparisons
 
-## To do
+## TODO
 
 * `smeval_neg` and `smeval_intCast` for `R` a ring and `S` an `AddCommGroup`.
 * Nonunital evaluation for polynomials with vanishing constant term for `Pow S ℕ+` (different file?)

diff --git a/Mathlib/Algebra/Quandle.lean b/Mathlib/Algebra/Quandle.lean
@@ -67,7 +67,7 @@ The following notation is localized in `quandles`:
 
 Use `open quandles` to use these.
 
-## Todo
+## TODO
 
 * If `g` is the Lie algebra of a Lie group `G`, then `(x ◃ y) = Ad (exp x) x` forms a quandle.
 * If `X` is a symmetric space, then each point has a corresponding involution that acts on `X`,

diff --git a/Mathlib/Algebra/Vertex/HVertexOperator.lean b/Mathlib/Algebra/Vertex/HVertexOperator.lean
@@ -16,7 +16,7 @@ here allows us to consider composites and scalar-multiply by multivariable Laure
 * The coefficient function as an `R`-linear map.
 ## Main results
 * Ext
-## To do:
+## TODO
 * Composition of heterogeneous vertex operators - values are Hahn series on lex order product
   (needs PR#10781).
 * `HahnSeries Γ R`-module structure on `HVertexOperator Γ R V W` (needs PR#10846).  This means we

diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean
@@ -18,7 +18,7 @@ We construct various limits and colimits in the category of schemes.
 * The preceding two results imply that `Scheme` has all finite limits.
 * The empty scheme is the (strict) initial object.
 
-## Todo
+## TODO
 
 * Coproducts exists (and the forgetful functors preserve them).
 

diff --git a/Mathlib/Analysis/InnerProductSpace/NormPow.lean b/Mathlib/Analysis/InnerProductSpace/NormPow.lean
@@ -13,7 +13,7 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
 In this file we prove that `x ↦ ‖x‖ ^ p` is continuously differentiable for
 an inner product space and for a real number `p > 1`.
 
-## Todo:
+## TODO
 * `x ↦ ‖x‖ ^ p` should be `C^n` for `p > n`.
 
 -/

diff --git a/Mathlib/Analysis/LocallyConvex/AbsConvex.lean b/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
@@ -26,7 +26,7 @@ of zero.
 * `with_gaugeSeminormFamily`: the topology of a locally convex space is induced by the family
 `gaugeSeminormFamily`.
 
-## Todo
+## TODO
 
 * Define the disked hull
 

diff --git a/Mathlib/Analysis/LocallyConvex/StrongTopology.lean b/Mathlib/Analysis/LocallyConvex/StrongTopology.lean
@@ -18,7 +18,7 @@ locally convex.
 
 * [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987]
 
-## Todo
+## TODO
 
 * Characterization in terms of seminorms
 

diff --git a/Mathlib/Analysis/NormedSpace/WeakDual.lean b/Mathlib/Analysis/NormedSpace/WeakDual.lean
@@ -47,7 +47,7 @@ weak-* topology on (its type synonym) `WeakDual 𝕜 E`:
   Closed balls in the dual of a normed space `E` over `ℝ` or `ℂ` are compact in the weak-star
   topology.
 
-TODOs:
+## TODO
 * Add that in finite dimensions, the weak-* topology and the dual norm topology coincide.
 * Add that in infinite dimensions, the weak-* topology is strictly coarser than the dual norm
   topology.

diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
@@ -17,7 +17,7 @@ To this end, we derive the representation of `log (1+z)` as the integral of `1/(
 over the unit interval (`Complex.log_eq_integral`) and introduce notation
 `Complex.logTaylor n` for the Taylor polynomial up to degree `n-1`.
 
-### TODO
+## TODO
 
 Refactor using general Taylor series theory, once this exists in Mathlib.
 -/

diff --git a/Mathlib/CategoryTheory/Bicategory/Adjunction.lean b/Mathlib/CategoryTheory/Bicategory/Adjunction.lean
@@ -32,7 +32,7 @@ identity maps or applying the pentagon relation. Such a hack may not be necessar
 coherence tactic is improved. One possible way would be to perform such a simplification in the
 preprocessing of the coherence tactic.
 
-## Todo
+## TODO
 
 * `Bicategory.mkOfAdjointifyUnit`: construct an adjoint equivalence from 2-isomorphisms
   `η : 𝟙 a ≅ f ≫ g` and `ε : g ≫ f ≅ 𝟙 b`, by upgrading `η` to a unit.

diff --git a/Mathlib/CategoryTheory/CofilteredSystem.lean b/Mathlib/CategoryTheory/CofilteredSystem.lean
@@ -41,7 +41,7 @@ Given a functor `F : J ⥤ Type v`:
 * `surjective_toEventualRanges` shows that if `F` is Mittag-Leffler, then `F.toEventualRanges`
   has all morphisms `F.map f` surjective.
 
-## Todo
+## TODO
 
 * Prove [Stacks: Lemma 0597](https://stacks.math.columbia.edu/tag/0597)
 

diff --git a/Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
@@ -17,7 +17,7 @@ import Mathlib.Logic.Equiv.Fin
 If a category has binary products and a terminal object then it has finite products.
 If a functor preserves binary products and the terminal object then it preserves finite products.
 
-# TODO
+## TODO
 
 Provide the dual results.
 Show the analogous results for functors which reflect or create (co)limits.

diff --git a/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean b/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
@@ -25,7 +25,7 @@ Similarly, if it has all finite products, and all equalizers, then it has all fi
 If a functor preserves all products and equalizers, then it preserves all limits.
 Similarly, if it preserves all finite products and equalizers, then it preserves all finite limits.
 
-# TODO
+## TODO
 
 Provide the dual results.
 Show the analogous results for functors which reflect or create (co)limits.

diff --git a/Mathlib/CategoryTheory/Limits/IndYoneda.lean b/Mathlib/CategoryTheory/Limits/IndYoneda.lean
@@ -22,7 +22,7 @@ Notation: categories `C`, `I` and functors `D : Iᵒᵖ ⥤ C`, `F : C ⥤ Type`
 - `colimitCoyonedaHomIsoLimit'`: a variant of `colimitCoyonedaHomIsoLimit` for a covariant
   diagram.
 
-## TODO:
+## TODO
 
 - define the ind-yoneda versions (for contravariant `F`)
 

diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean
@@ -41,7 +41,7 @@ For convenience, we work directly with finite types instead of natural numbers.
 allows us to work directly with `α`, `Option α`, `(ι → α) → κ`, and `ι ⊕ ι'` instead of `Fin n`,
 `Fin (n+1)`, `Fin (c^(n^H))`, and `Fin (H + H')`.
 
-## Todo
+## TODO
 
 - Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the
 current proof).

diff --git a/Mathlib/Combinatorics/Hall/Basic.lean b/Mathlib/Combinatorics/Hall/Basic.lean
@@ -43,7 +43,7 @@ The core of this module is constructing the inverse system: for every finite sub
   `r : α → β → Prop` on finite types, with the Hall condition given in terms of
   `finset.univ.filter`.
 
-## Todo
+## TODO
 
 * The statement of the theorem in terms of bipartite graphs is in preparation.
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -29,7 +29,7 @@ This module defines simple graphs on a vertex type `V` as an irreflexive symmetr
   `CompleteAtomicBooleanAlgebra`. In other words, this is the complete lattice of spanning subgraphs
   of the complete graph.
 
-## Todo
+## TODO
 
 * This is the simplest notion of an unoriented graph.  This should
   eventually fit into a more complete combinatorics hierarchy which

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
@@ -42,7 +42,7 @@ a complete graph, whose vertices represent the colors.
 
 * `C.colorClasses` is the set containing all color classes.
 
-## Todo:
+## TODO
 
   * Gather material from:
     * https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/coloring.lean

diff --git a/Mathlib/Combinatorics/SimpleGraph/Metric.lean b/Mathlib/Combinatorics/SimpleGraph/Metric.lean
@@ -18,7 +18,7 @@ pairs of vertices to the length of the shortest walk between them.
 
 - `SimpleGraph.dist` is the graph metric.
 
-## Todo
+## TODO
 
 - Provide an additional computable version of `SimpleGraph.dist`
   for when `G` is connected.

diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@@ -41,7 +41,7 @@ sub-relation of the adjacency relation of the simple graph.
 * Recall that subgraphs are not determined by their vertex sets, so `SetLike` does not apply to
   this kind of subobject.
 
-## Todo
+## TODO
 
 * Images of graph homomorphisms as subgraphs.
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Trails.lean b/Mathlib/Combinatorics/SimpleGraph/Trails.lean
@@ -25,7 +25,7 @@ as Eulerian circuits).
 * `SimpleGraph.Walk.IsEulerian.card_odd_degree` gives the possible numbers of odd-degree
   vertices when there exists an Eulerian trail.
 
-## Todo
+## TODO
 
 * Prove that there exists an Eulerian trail when the conclusion to
   `SimpleGraph.Walk.IsEulerian.card_odd_degree` holds.

diff --git a/Mathlib/Data/List/Sym.lean b/Mathlib/Data/List/Sym.lean
@@ -18,7 +18,7 @@ from a given list. These are list versions of `Nat.multichoose`.
 * `List.sym2`: `xs.sym2` is a list of all unordered pairs of elements from `xs`,
   with multiplicity. The list's values are in `Sym2 α`.
 
-## Todo
+## TODO
 
 * Prove `protected theorem Perm.sym (n : ℕ) {xs ys : List α} (h : xs ~ ys) : xs.sym n ~ ys.sym n`
   and lift the result to `Multiset` and `Finset`.

diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean
@@ -9,7 +9,7 @@ import Mathlib.Data.Set.Lattice
 #align_import data.nat.pairing from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432"
 
 /-!
-#  Naturals pairing function
+# Naturals pairing function
 
 This file defines a pairing function for the naturals as follows:
 ```text

diff --git a/Mathlib/Data/Real/Pointwise.lean b/Mathlib/Data/Real/Pointwise.lean
@@ -17,7 +17,7 @@ This file relates `sInf (a • s)`/`sSup (a • s)` with `a • sInf s`/`a • s
 From these, it relates `⨅ i, a • f i` / `⨆ i, a • f i` with `a • (⨅ i, f i)` / `a • (⨆ i, f i)`,
 and provides lemmas about distributing `*` over `⨅` and `⨆`.
 
-# TODO
+## TODO
 
 This is true more generally for conditionally complete linear order whose default value is `0`. We
 don't have those yet.

diff --git a/Mathlib/Data/Rel.lean b/Mathlib/Data/Rel.lean
@@ -32,7 +32,7 @@ Relations are also known as set-valued functions, or partial multifunctions.
 * `Rel.restrict_domain`: Domain-restriction of a relation to a subtype.
 * `Function.graph`: Graph of a function as a relation.
 
-## TODOs
+## TODO
 
 The `Rel.comp` function uses the notation `r • s`, rather than the more common `r ∘ s` for things
 named `comp`. This is because the latter is already used for function composition, and causes a

diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean
@@ -22,7 +22,7 @@ This file introduces the commuting probability of finite groups.
 ## Main definitions
 * `commProb`: The commuting probability of a finite type with a multiplication operation.
 
-## Todo
+## TODO
 * Neumann's theorem.
 -/
 

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
@@ -17,7 +17,7 @@ algebras, as `CliffordAlgebra.equivProd`.
 
 * `CliffordAlgebra.equivProd : CliffordAlgebra (Q₁.prod Q₂) ≃ₐ[R] (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)`
 
-## TODO:
+## TODO
 
 Introduce morphisms and equivalences of graded algebas, and upgrade `CliffordAlgebra.equivProd` to a
 graded algebra equivalence.

diff --git a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
@@ -25,7 +25,7 @@ This file defines the conversion between sesquilinear forms and matrices.
  * `LinearMap.toMatrix₂`: calculate the matrix coefficients of a bilinear form
  * `LinearMap.toMatrix₂'`: calculate the matrix coefficients of a bilinear form on `n → R`
 
-## Todos
+## TODO
 
 At the moment this is quite a literal port from `Matrix.BilinearForm`. Everything should be
 generalized to fully semibilinear forms.

diff --git a/Mathlib/LinearAlgebra/RootSystem/Basic.lean b/Mathlib/LinearAlgebra/RootSystem/Basic.lean
@@ -23,7 +23,7 @@ This file contains basic results for root systems and root data.
    roots form a root system, we do not need to check that the coroots are stable under reflections
    since this follows from the corresponding property for the roots.
 
-## Todo
+## TODO
 
 * Derived properties of pairs, e.g., (ultra)parallel linearly independent pairs generate infinite
    dihedral groups.

diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/Mathlib/LinearAlgebra/RootSystem/Defs.lean
@@ -27,7 +27,7 @@ This file contains basic definitions for root systems and root data.
  * `RootPairing.IsReduced`: A root pairing is said to be reduced if it never contains the double of
    a root.
 
-## Todo
+## TODO
 
 * Put more API theorems in the Defs file.
 * Introduce the Weyl Group, and its action on the indexing set.

diff --git a/Mathlib/MeasureTheory/Function/LpOrder.lean b/Mathlib/MeasureTheory/Function/LpOrder.lean
@@ -11,11 +11,11 @@ import Mathlib.MeasureTheory.Function.LpSpace
 /-!
 # Order related properties of Lp spaces
 
-### Results
+## Results
 
 - `Lp E p μ` is an `OrderedAddCommGroup` when `E` is a `NormedLatticeAddCommGroup`.
 
-### TODO
+## TODO
 
 - move definitions of `Lp.posPart` and `Lp.negPart` to this file, and define them as
   `PosPart.pos` and `NegPart.neg` given by the lattice structure.

diff --git a/Mathlib/MeasureTheory/Group/Arithmetic.lean b/Mathlib/MeasureTheory/Group/Arithmetic.lean
@@ -36,7 +36,7 @@ For the heuristics of `@[to_additive]` it is important that the type with a mult
 
 measurable function, arithmetic operator
 
-## Todo
+## TODO
 
 * Uniformize the treatment of `pow` and `smul`.
 * Use `@[to_additive]` to send `MeasurablePow` to `MeasurableSMul₂`.

diff --git a/Mathlib/MeasureTheory/Integral/Indicator.lean b/Mathlib/MeasureTheory/Integral/Indicator.lean
@@ -16,7 +16,7 @@ This file has a few measure theoretic or integration-related results on indicato
 This file exists to avoid importing `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable`
 in `Mathlib.MeasureTheory.Integral.Lebesgue`.
 
-## Todo
+## TODO
 
 The result `MeasureTheory.tendsto_measure_of_tendsto_indicator` here could be proved without
 integration, if we had convergence of measures results for countably generated filters. Ideally,

diff --git a/Mathlib/MeasureTheory/Integral/Marginal.lean b/Mathlib/MeasureTheory/Integral/Marginal.lean
@@ -48,7 +48,7 @@ set `s` of integration variables is a `Finset`. We are assuming that the functio
 for most of this file. Note that asking whether it is `AEMeasurable` is not even well-posed,
 since there is no well-behaved measure on the domain of `f`.
 
-## Todo
+## TODO
 
 * Define the marginal function for functions taking values in a Banach space.
 

diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@@ -20,7 +20,7 @@ the underlying space is metrizable and separable.
 * `MeasureTheory.FiniteMeasure.prod`: The product of two finite measures.
 * `MeasureTheory.ProbabilityMeasure.prod`: The product of two probability measures.
 
-## Todo
+## TODO
 
 * Add continuous dependence of the product measures on the factors.
 

diff --git a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
@@ -28,7 +28,7 @@ import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
   probability measures on a separable space coincides with the topology of convergence in
   distribution, and in particular convergence in distribution is then pseudometrizable.
 
-## Todo
+## TODO
 
 * Show that in Borel spaces, the Lévy-Prokhorov distance is a metric; not just a pseudometric.
 

diff --git a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
@@ -44,7 +44,7 @@ Although I don't know whether it's of any use, `ModularCyclotomicCharacter'`
 is the general case for integral domains, with target in `(ZMod d)ˣ`
 where `d` is the number of `n`th roots of unity in `L`.
 
-## Todo
+## TODO
 
 * Prove the compatibility of `ModularCyclotomicCharacter n` and `ModularCyclotomicCharacter m`
   if `n ∣ m`.

diff --git a/Mathlib/NumberTheory/WellApproximable.lean b/Mathlib/NumberTheory/WellApproximable.lean
@@ -48,7 +48,7 @@ We do *not* include a formalisation of the Koukoulopoulos-Maynard result here.
  * `NormedAddCommGroup.exists_norm_nsmul_le`: a general version of Dirichlet's approximation theorem
  * `AddCircle.exists_norm_nsmul_le`: Dirichlet's approximation theorem
 
-## TODO:
+## TODO
 
 The hypothesis `hδ` in `AddCircle.addWellApproximable_ae_empty_or_univ` can be dropped.
 An elementary (non-measure-theoretic) argument shows that if `¬ hδ` holds then

diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean
@@ -15,7 +15,7 @@ We define the predicate `Order.IsSuccLimit` for "successor limits", values that
 others. They are so named since they can't be the successors of anything smaller. We define
 `Order.IsPredLimit` analogously, and prove basic results.
 
-## Todo
+## TODO
 
 The plan is to eventually replace `Ordinal.IsLimit` and `Cardinal.IsLimit` with the common
 predicate `Order.IsSuccLimit`.