From ca8d01ba35e1f67c1b01bf9e637d7b01d89e020c Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 9 Jul 2024 22:47:57 +0000 Subject: [PATCH] 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 --- Mathlib/Algebra/Group/NatPowAssoc.lean | 2 +- Mathlib/Algebra/Group/PNatPowAssoc.lean | 2 +- .../Algebra/Homology/DerivedCategory/SingleTriangle.lean | 2 +- Mathlib/Algebra/Order/Module/Algebra.lean | 2 +- Mathlib/Algebra/Polynomial/Smeval.lean | 2 +- Mathlib/Algebra/Quandle.lean | 2 +- Mathlib/Algebra/Vertex/HVertexOperator.lean | 2 +- Mathlib/AlgebraicGeometry/Limits.lean | 2 +- Mathlib/Analysis/InnerProductSpace/NormPow.lean | 2 +- Mathlib/Analysis/LocallyConvex/AbsConvex.lean | 2 +- Mathlib/Analysis/LocallyConvex/StrongTopology.lean | 2 +- Mathlib/Analysis/NormedSpace/WeakDual.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean | 2 +- Mathlib/CategoryTheory/Bicategory/Adjunction.lean | 2 +- Mathlib/CategoryTheory/CofilteredSystem.lean | 2 +- .../Constructions/FiniteProductsOfBinaryProducts.lean | 2 +- .../Limits/Constructions/LimitsOfProductsAndEqualizers.lean | 2 +- Mathlib/CategoryTheory/Limits/IndYoneda.lean | 2 +- Mathlib/Combinatorics/HalesJewett.lean | 2 +- Mathlib/Combinatorics/Hall/Basic.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Coloring.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Metric.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Trails.lean | 2 +- Mathlib/Data/List/Sym.lean | 2 +- Mathlib/Data/Nat/Pairing.lean | 2 +- Mathlib/Data/Real/Pointwise.lean | 2 +- Mathlib/Data/Rel.lean | 2 +- Mathlib/GroupTheory/CommutingProbability.lean | 2 +- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean | 2 +- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean | 2 +- Mathlib/LinearAlgebra/RootSystem/Basic.lean | 2 +- Mathlib/LinearAlgebra/RootSystem/Defs.lean | 2 +- Mathlib/MeasureTheory/Function/LpOrder.lean | 4 ++-- Mathlib/MeasureTheory/Group/Arithmetic.lean | 2 +- Mathlib/MeasureTheory/Integral/Indicator.lean | 2 +- Mathlib/MeasureTheory/Integral/Marginal.lean | 2 +- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean | 2 +- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean | 2 +- Mathlib/NumberTheory/WellApproximable.lean | 2 +- Mathlib/Order/SuccPred/Limit.lean | 2 +- Mathlib/Probability/Density.lean | 2 +- Mathlib/Probability/Distributions/Uniform.lean | 2 +- Mathlib/RepresentationTheory/Character.lean | 4 ++-- Mathlib/RingTheory/ChainOfDivisors.lean | 2 +- Mathlib/RingTheory/Henselian.lean | 2 +- Mathlib/RingTheory/Ideal/AssociatedPrime.lean | 2 +- Mathlib/RingTheory/IntegrallyClosed.lean | 2 +- Mathlib/RingTheory/UniqueFactorizationDomain.lean | 2 +- Mathlib/SetTheory/Ordinal/Principal.lean | 6 +++--- Mathlib/SetTheory/Surreal/Basic.lean | 2 +- Mathlib/SetTheory/ZFC/Ordinal.lean | 2 +- Mathlib/Tactic/Linter/UnusedTactic.lean | 6 +++--- Mathlib/Tactic/NormNum/BigOperators.lean | 2 +- Mathlib/Topology/Bases.lean | 2 +- Mathlib/Topology/Separation.lean | 2 +- 58 files changed, 64 insertions(+), 64 deletions(-) diff --git a/Mathlib/Algebra/Group/NatPowAssoc.lean b/Mathlib/Algebra/Group/NatPowAssoc.lean index a713ff185ff00..2a021cdc2f6ca 100644 --- 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 index 3e32256dbea83..d87d4474a1756 100644 --- 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 index c1eaf214e0112..e4d1eff8ac407 100644 --- 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 index ec005d0ea7cfe..079e1ce13f6fa 100644 --- 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 index 74bb41b6fe9b5..3405de87423d4 100644 --- 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 index aa8118e3c7549..6d24f3a349808 100644 --- 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 index 65f34173b0689..213329acd5a92 100644 --- 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 index 42f093f9aa527..455eed5933dfd 100644 --- 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 index 5bfdc5f36322f..bf01e70b29384 100644 --- 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 index ea2311fbef245..c69cf0cc727e5 100644 --- 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 index 614ae43902f77..166d79da3d4e6 100644 --- 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 index 84eaf387dba26..808e484e9357e 100644 --- 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 index 11fb8a4ea158f..09d09fd116e68 100644 --- 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 index bff2a8418abcb..13595c76a857a 100644 --- 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 index 8c0f2793a55ed..f686e8c4d80b7 100644 --- 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 index 7fcbf8a092540..b37fb031c42ea 100644 --- 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 index 4555d28a5c9fe..015586f7cf37c 100644 --- 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 index 6badc24faa07e..99842d2a0d02f 100644 --- 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 index f741cd0f1234f..5eb3c9536488b 100644 --- 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 index d7f336e7c4e11..8a34820f8c8dc 100644 --- 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 index da23022aa98c3..285343237e915 100644 --- 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 index 0bca249e74346..d1d542b11c4d7 100644 --- 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 index 0c52b38c2d2f8..b79730e3ba297 100644 --- 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 index fe2da14ea3a66..7ba8880d69cad 100644 --- 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 index 7b12a152f96d4..f3663604d14d5 100644 --- 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 index f3de3a320aed7..6f9ad045b52fb 100644 --- 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 index 8f796ad0b9762..274926bbaee22 100644 --- 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 index 1dd16cd89328e..b429a32defc24 100644 --- 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 index 0dd20a97f7cf3..ceedf4a9638c1 100644 --- 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 index dbb6c51855ba9..b613345b7c2c8 100644 --- 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 index cf803e0bf338b..39f752d0f3bf9 100644 --- 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 index 7180f56ba5979..1acb748b4aea7 100644 --- 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 index f693c35176982..a6376901bcdf1 100644 --- 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 index 8d79fdb70eefc..8ce5eed7055ed 100644 --- 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 index c851e17cf7184..f2c34a0fdaba0 100644 --- 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 index f660ed01617f2..69ae08745332e 100644 --- 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 index 0c43ee10dd403..fb1889b30f770 100644 --- 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 index b0eb900877c25..ebbbb2919404f 100644 --- 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 index f9006a191146e..5ec34e572fd68 100644 --- 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 index 836b661fb9d2c..7dd2d9895eb47 100644 --- 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 index 6a01eeb26f11b..1f7a73c505206 100644 --- 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 index bf65b8ddd0a05..6d864bf99d111 100644 --- 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 index d778ab7a3bcf2..b0c684eb8483f 100644 --- 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`. diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean index 661c9587c3486..fbe5cf477570a 100644 --- a/Mathlib/Probability/Density.lean +++ b/Mathlib/Probability/Density.lean @@ -44,7 +44,7 @@ random variables with this distribution. its pdf having support `s`, then `X` has expectation `(λ s)⁻¹ * ∫ x in s, x dx` where `λ` is the Lebesgue measure. -## TODOs +## TODO Ultimately, we would also like to define characteristic functions to describe distributions as it exists for all random variables. However, to define this, we will need Fourier transforms diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean index 6c4290bfe3e56..78e512d976746 100644 --- a/Mathlib/Probability/Distributions/Uniform.lean +++ b/Mathlib/Probability/Distributions/Uniform.lean @@ -35,7 +35,7 @@ This file defines a number of uniform `PMF` distributions from various inputs, `PMF.ofMultiset` draws randomly from the given `Multiset`, treating duplicate values as distinct. Each probability is given by the count of the element divided by the size of the `Multiset` -# To Do: +## TODO * Refactor the `PMF` definitions to come from a `uniformMeasure` on a `Finset`/`Fintype`/`Multiset`. -/ diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean index 57b65f29b9589..fae9ee32d1b15 100644 --- a/Mathlib/RepresentationTheory/Character.lean +++ b/Mathlib/RepresentationTheory/Character.lean @@ -19,12 +19,12 @@ A key result is the orthogonality of characters for irreducible representations over an algebraically closed field whose characteristic doesn't divide the order of the group. It is the theorem `char_orthonormal` -# Implementation notes +## Implementation notes Irreducible representations are implemented categorically, using the `Simple` class defined in `Mathlib.CategoryTheory.Simple` -# TODO +## TODO * Once we have the monoidal closed structure on `FdRep k G` and a better API for the rigid structure, `char_dual` and `char_linHom` should probably be stated in terms of `Vᘁ` and `ihom V W`. -/ diff --git a/Mathlib/RingTheory/ChainOfDivisors.lean b/Mathlib/RingTheory/ChainOfDivisors.lean index 90fc2854d0b25..5c33525bc43a4 100644 --- a/Mathlib/RingTheory/ChainOfDivisors.lean +++ b/Mathlib/RingTheory/ChainOfDivisors.lean @@ -29,7 +29,7 @@ and the set of factors of `a`. `multiplicity p a = multiplicity (d p) b` -## Todo +## TODO - Create a structure for chains of divisors. - Simplify proof of `mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors` using `mem_normalizedFactors_factor_order_iso_of_mem_normalizedFactors` or vice versa. diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean index 8ac1ef761694e..35103de60586d 100644 --- a/Mathlib/RingTheory/Henselian.lean +++ b/Mathlib/RingTheory/Henselian.lean @@ -42,7 +42,7 @@ In this case the first condition is automatic, and in the second condition we ma https://stacks.math.columbia.edu/tag/04GE -## Todo +## TODO After a good API for etale ring homomorphisms has been developed, we can give more equivalent characterization of Henselian rings. diff --git a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean index 81d281462c987..df0b31b8c173f 100644 --- a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean +++ b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean @@ -27,7 +27,7 @@ We provide the definition and related lemmas about associated primes of modules. - `associatedPrimes.eq_singleton_of_isPrimary`: In a noetherian ring, `I.radical` is the only associated prime of `R ⧸ I` when `I` is primary. -## Todo +## TODO Generalize this to a non-commutative setting once there are annihilator for non-commutative rings. diff --git a/Mathlib/RingTheory/IntegrallyClosed.lean b/Mathlib/RingTheory/IntegrallyClosed.lean index e816a9595e247..ddeed135bec6e 100644 --- a/Mathlib/RingTheory/IntegrallyClosed.lean +++ b/Mathlib/RingTheory/IntegrallyClosed.lean @@ -24,7 +24,7 @@ integral over `R`. A special case of integrally closed rings are the Dedekind do * `isIntegrallyClosed_iff K`, where `K` is a fraction field of `R`, states `R` is integrally closed iff it is the integral closure of `R` in `K` -## TODO: Related notions +## TODO Related notions The following definitions are closely related, especially in their applications in Mathlib. diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index 5c7eda2f2a731..22910dc13f5d2 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -22,7 +22,7 @@ import Mathlib.RingTheory.Multiplicity * `UniqueFactorizationMonoid` holds for `WfDvdMonoid`s where `Irreducible` is equivalent to `Prime` -## To do +## TODO * set up the complete lattice structure on `FactorSet`. -/ diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean index 833f25df08bd4..daca259971d10 100644 --- a/Mathlib/SetTheory/Ordinal/Principal.lean +++ b/Mathlib/SetTheory/Ordinal/Principal.lean @@ -8,11 +8,11 @@ import Mathlib.SetTheory.Ordinal.FixedPoint #align_import set_theory.ordinal.principal from "leanprover-community/mathlib"@"31b269b60935483943542d547a6dd83a66b37dc7" /-! -### Principal ordinals +# Principal ordinals We define principal or indecomposable ordinals, and we prove the standard properties about them. -### Main definitions and results +## Main definitions and results * `Principal`: A principal or indecomposable ordinal under some binary operation. We include 0 and any other typically excluded edge cases for simplicity. * `unbounded_principal`: Principal ordinals are unbounded. @@ -21,7 +21,7 @@ We define principal or indecomposable ordinals, and we prove the standard proper * `principal_mul_iff_le_two_or_omega_opow_opow`: The main characterization theorem for multiplicative principal ordinals. -### Todo +## TODO * Prove that exponential principal ordinals are 0, 1, 2, ω, or epsilon numbers, i.e. fixed points of `fun x ↦ ω ^ x`. -/ diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean index fb326c47ef41e..1ac7ec0261df2 100644 --- a/Mathlib/SetTheory/Surreal/Basic.lean +++ b/Mathlib/SetTheory/Surreal/Basic.lean @@ -37,7 +37,7 @@ surreals form a linear ordered commutative ring. One can also map all the ordinals into the surreals! -### Todo +## TODO - Define the field structure on the surreals. diff --git a/Mathlib/SetTheory/ZFC/Ordinal.lean b/Mathlib/SetTheory/ZFC/Ordinal.lean index 44c2bc5cfe81d..6a5b20348d0e1 100644 --- a/Mathlib/SetTheory/ZFC/Ordinal.lean +++ b/Mathlib/SetTheory/ZFC/Ordinal.lean @@ -19,7 +19,7 @@ Further development can be found on the branch `von_neumann_v2`. - `ZFSet.IsTransitive` means that every element of a set is a subset. -## Todo +## TODO - Define von Neumann ordinals. - Define the basic arithmetic operations on ordinals from a purely set-theoretic perspective. diff --git a/Mathlib/Tactic/Linter/UnusedTactic.lean b/Mathlib/Tactic/Linter/UnusedTactic.lean index 2dfcdac0c14f4..fb57a6ed99fd2 100644 --- a/Mathlib/Tactic/Linter/UnusedTactic.lean +++ b/Mathlib/Tactic/Linter/UnusedTactic.lean @@ -9,7 +9,7 @@ import Batteries.Data.List.Basic import Batteries.Tactic.Unreachable /-! -# The unused tactic linter +# The unused tactic linter The unused linter makes sure that every tactic call actually changes *something*. @@ -29,7 +29,7 @@ The only tactic that has a bespoke criterion is `swap_var`: the reason is that t Thus, to check that `swap_var` was used, so we inspect the names of all the local declarations before and after and see if there is some change. -### Notable exclusions +## Notable exclusions * `conv` is completely ignored by the linter. @@ -43,7 +43,7 @@ before and after and see if there is some change. The main reason is that `skip` is a common discharger tactic and the linter would then always fail whenever the user explicitly chose to pass `skip` as a discharger tactic. -### TODO +## TODO * The linter seems to be silenced by `set_option ... in`: maybe it should enter `in`s? ## Implementation notes diff --git a/Mathlib/Tactic/NormNum/BigOperators.lean b/Mathlib/Tactic/NormNum/BigOperators.lean index 9de2a56fd9c75..1a05d67ebc0df 100644 --- a/Mathlib/Tactic/NormNum/BigOperators.lean +++ b/Mathlib/Tactic/NormNum/BigOperators.lean @@ -30,7 +30,7 @@ This plugin is noticeably less powerful than the equivalent version in Mathlib 3 In particular, we can't use the plugin on sums containing variables. (See also the TODO note "To support variables".) -## TODOs +## TODO * Support intervals: `Finset.Ico`, `Finset.Icc`, ... * To support variables, like in Mathlib 3, turn this into a standalone tactic that unfolds diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 550600e2345da..1a86854259f86 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -46,7 +46,7 @@ conditions are equivalent in this case). For our applications we are interested that there exists a countable basis, but we do not need the concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins. -### TODO: +## TODO More fine grained instances for `FirstCountableTopology`, `TopologicalSpace.SeparableSpace`, and more. diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index d1de1216dc4c6..1895a1df6a8ed 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -56,7 +56,7 @@ This file defines the predicate `SeparatedNhds`, and common separation axioms Note that `mathlib` adopts the modern convention that `m ≤ n` if and only if `T_m → T_n`, but occasionally the literature swaps definitions for e.g. T₃ and regular. -### TODOs +### TODO * Add perfectly normal and T6 spaces. * Use `hasSeparatingCovers_iff_separatedNhds` to prove that perfectly normal spaces