Small TODOs to do!

[ericrbg]

Key: SP = small project, SC = small chore.

This is a list of a bunch of todos in a semi-disorganised way; I've been going through literally every occurence of the string "todo". These were chosen to specifically be quite small and limited in scope, and the hope is that most can be done in <1hr each, very often much less. I thought it'd be helpful to provide an easy way to access a long list of things to fix in Mathlib when you have a couple seconds here or there (or as the inspriation for this started, on somewhere like the Tube!). If you PR a fix to any of these, I'd appreciate editing the PR number into the issue, so that it is easy for others to keep track of.

I haven't finished going through the whole list yet, so I will probably add far more with time:)

Re SP, SC: I feel like these are small mini things that are hopefully rewarding and not too awful to do. Some of these are chosen according to what I know well - there may be many more SPs in category theory, for example, but I'm mega unfamiliar with that part of the library, so I didn't want to send people on a wild goose chase!

Todos:

• [ ] Algebra/Algebra/Basic: #8017

• [ ] Algebra/Algebra/Unitization: essential ideal not defined; also the actual ideal also doesn’t seem to be defined?

• [ ] Algebra/Algebra/Subalgebra: iSupLift seems easy to do

• [ ] Algebra/Algebra/Subalgebra/Unitization: why is subring not a NonAssocRing thing?

• [ ] Algebra/BigOperators/Basic: Scoped[NS] is implemented!

• [ ] Algebra/BigOperators/Order: to_additive duplication doesn’t seem to happen anymore!

• [ ] Algebra/Category/GroupCat: don’t we have ulift instances already?

• [ ] Algebra/CharP/MixedCharZero: “Relate mixed characteristic in a local ring to p-adic numbers” - what is the link?

• [ ] Algebra/DirectSum/Basic: what is meant by this?

• [ ] def setToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, β i) →+ ⨁ i : T, β i := without S ⊆ T seems nonsensical.

• [ ] Algebra/FreeMonoid/Basic: run CI when landing

• [ ] Algebra/GroupPower/Lemmas: can provide NoZeroSMulDivisors later.

• [ ] Algebra/Hom/Freiman: map_multiset_prod seems generalised, but not sure if this instance is advisable

• [ ] Algebra/Lie/Killing: SP, see https://math.stackexchange.com/questions/2248503/proof-that-the-killing-form-on-a-simple-lie-algebra-is-non-degenerate

• [ ] Algebra/Lie/Subalgebra: SP #7994

• [ ] Algebra/Module/Projective.lean: 1/2,3: SP/universes

• [ ] Algebra/Order/Floor: SC

• [ ] Algebra/Order/Kleene: SC

• [ ] Algebra/Order/SMul: should be easy to write but may be slow!

• [ ] Algebra/Order/WithZero: check/remove

• [ ] Algebra/Order/Field: small generalisations

• [ ] Algebra/Order/Monoid/Canonical/Defs: should exist? if not check already

• [ ] Algebra/Order/Ring/Canonical: this can enable Odd.tsub, however it may also be too much — Odd.tsub can be achieved with a refactor of Odd to use only Add and One.

• [ ] Algebra/Order/Ring/Lemmas: easy to make local with scoped notation now

• [ ] Algebra/Order/Ring/WithTop: it doesn’t even work now, maybe remove todo?

• [ ] Algebra/Order/Sub/Defs: SP to generalise nat lemmas

• [ ] Algebra/Ring/BooleanRing: we can lower priority now I think?

• [ ] Algebra/Star/Module: can these be made simp?

• [ ] AlgebraicTopology/FundamentalGroupoid: make issue?

• [x] Analysis/BoundedVariation: rfl now works: #8145

• [ ] Analysis/Seminorm: should be easy!

• [ ] Analysis/BoxIntegral/Partition/Filter: maybe SP? unfamiliar with this area

• [ ] Analysis/Calculus/ContDiff: -- porting note: TODO: define Neg instance on ContinuousLinearEquiv should be easy?

• [ ] ContDiffWithinAt.div: also easy?

• [ ] Analysis/Complex/PhragmenLindelof: fun investigation

• [ ] Analysis/Convex/Exposed, Extreme: @YaelDillies what’s the lean4 status of this?

• [ ] Analysis/Convex/SpecificFunctions/Basic,Pow: SP

• [ ] Analysis/Fourier/PoissonSummation: do we have that the fourier transform preserve Schwartz? no, this is somewhat involved

• [x] Analysis/InnerProductSpace/Adjoint: #8295

• [ ] Analysis/Normed/Group/ControlledClosure: possible SP

• [ ] Analysis/NormedSpace/Banach: do we have quotient normed spaces?

• [ ] Analysis/NormedSpace/lpSpace: Holder: SP; investigate IsLUB API.

• [ ] Analysis/NormedSpace/Star/Basic: SP

• [ ] Analysis/SpecialFunctions/Exp: remove mentions of backporting; try making @[simp].

• [ ] Analysis/SpecialFunctions/Log/Monotone: SP

• [ ] CategoryTheory/Skeletal: may exist by now?

• [ ] CategoryTheory/Limits/Shapes/Biproducts: 2: SP

• [ ] CategoryTheory/Limits/Shapes/Terminal: SP

• [ ] CategoryTheory/Monoidal/Center: can this be done easily?

• [ ] CategoryTheory/Sites/SheafOfTypes: maybe easy

• [ ] Combinatorics/Composition: SC

• [ ] Combinatorics/Configuration: just check?

• [ ] Combinatorics/Additive/SalemSpencer: if possible, I assume obvious?

• [ ] Combinatorics/Quiver/Covering: SC

• [ ] Combinatorics/SetFamily/Shadow: SP

• [ ] Combinatorics/SimpleGraph/AdjMatrix: check ML:3024

• [ ] Combinatorics/SimpleGraph/Coloring: 2: in theory doable but seems computationally ridiculous? 3-4: what’s the proposed refactor of chromatic numbers?

• [ ] Combinatorics/SimpleGraph/Regularity/{Chunk,Increment}: gcongr golf fiesta? SC (not really a chore LOL)

• [ ] Combinatorics/Young/YoungDiagram: what is “correct” here? SetLike experts

• [x] Data/Finmap: all should not return true for an empty Finmap, surely. #13227

• [ ] Data/Part: note down that it is control_laws_tac

• [ ] Data/Rel: image_eq does get proved by rfl; is this what’s meant?

• [ ] Data/Analysis/Filter: SC, docs

• [ ] Data/Complex/Basic: this NeZero instance can either be elsewhere or somehow gotten to in a different way

• [ ] Data/DFinsupp/Basic: can this be fixed? is this expected?

• [x] #8018

• [ ] Data/Finset/Card: isn’t the noncomputable version Nat.card?

• [ ] Data/Finset/Lattice: SC for first 3, the fourth one seems irrelevant

• [ ] Data/Finset/LocallyFinite: SP: prove that DenselyOrdered + LocallyFinite -> False. Then use this to prove the lemmas that have these assumptions, or try and remove them if possible. Also the one about id_eq - not sure what is meant. (the lemmas near this one can be golfed a tiny bit using le_rfl)

• [ ] Data/Finset/Pointwise, Data/Set/Pointwise/SMul: does such a typeclass exist yet?

• [ ] Data/Finset/Slice: SP

• [ ] Data/Finset/Sym: SP

• [ ] Data/Finsupp/Multiset: SP

• [ ] Data/Finsupp/Order: SC

• [ ] Data/Finsupp/Pointwise: look to see if generalization is sensible?

• [ ] Data/Fintype/Basic: ↥ is not here anymore.

• [ ] Data/Fintype/List: nodup_permutations seems to exist.

• [ ] Data/Int/Interval: can this be done? int.coe_nat_inj presumably exists

• [ ] Data/Int/Dvd/Pow: not sure why we wouldn’t?

• [ ] Data/List/AList: SC

• [ ] Data/List/Basic: SP: toChunks.

• [ ] Data/List/Perm: SP -List.nodup_permutation may be helpful?

• [ ] Data/List/Permutation: SC docs. List.nodup_permutation seems to come up a lot.

• [ ] Data/List/Rotate: SC, just check @[simp] compiles!

• [ ] Data/List/ToFinsupp: find/report a Lean4 bug here.

• [ ] Data/List/Operator/Basic: don’t we have tropical rings?

• [ ] Data/Matrix/{Basic,Block,Hadamard,Kronecker,PEquiv}: mathlib4#3024 is resolved,

• [ ] Data/Matrix/Basis: induction_on' seems unchangeable, as far as I can see

• [ ] Data/Multiset/Basic: move to near decidablePerm?

• [ ] Data/MvPolynomial/Equiv: I’m not sure they should be?

• [ ] Data/MvPolynomial/Variables: 1,2 SP

• [ ] Data/Nat/Bits: is this supported by norm_num anymore? should it be? transform this into new TODO

• [ ] Data/Nat/Factorization/Basic: SP/SC? not sure haha; also h1 should probably be in by now

• [ ] Data/Nat/Fib/Zeckendorf: open lean4 issue

• [ ] Data/Nat/Order: can this be upstreamed?

• [ ] Data/Polynomial/Basic: SC delete monomial_add

• [ ] Data/Polynomial/Coeff: does it cause import issues?

• [ ] Data/Polynomial/Eval: SC

• [ ] Data/Polynomial/Mirror: SC

• [ ] Data/Polynomial/Monic: this mathlib3-GH issue refers to Polynomial.opRingEquiv; SC

• [ ] Data/Polynomial/UnitTrinomial: SP

• [ ] Data/Polynomial/Degree/Definitions: try dedup, it may be that sum_fin ends up more useful, unsure

• [ ] Data/Rat/Defs: this align looks wrong anyways? unsure

• [ ] Data/Real/Basic: these variables are not.

• [ ] Data/Real/EReal: 1: isn’t it provided explicitly?

• [ ] Data/Real/NNReal: 23 check if can be deleted, 4 SP

• [ ] Data/Real/Sqrt: do we have a pp_nodot?

• [ ] Data/Set/Semiring: do we have a GH issue for the fact that funlikes can’t have dot notation? 2: what do you mean port?

• [ ] Data/Set/Pointwise/Basic: to_additive what?

• [ ] Data/Set/Pointwise/BigOperators: SP

• [ ] Data/Set/Pointwise/Interval: the notation doesn’t seem to be broken

• [ ] Data/Sigma/Order: SP

• [ ] #13572

• [ ] Data/ZMod/Basic: 1: is it worth making this equivalence work for all n? 2: SP

[BoltonBailey]

I'm going to add the good-first-issue tag to this so that newcomers can potentially find it more easily.

[BoltonBailey]

Data/Finmap: all should not return true for an empty Finmap, surely.

Surely it should, just as List.all does? I am confused by this one.

[ndcroos]

Great list! I'd like to work on Algebra/Order/Kleene.

[YaelDillies]

• Analysis/Convex/Exposed, Extreme: @YaelDillies what’s the lean4 status of this?

See #14655 for an update