Indep vs Independent

Stream: mathlib4

[Eric Wieser]

We currently have docs#SupIndep, docs#ProbabilityTheory.IndepFun, and docs#LinearIndependent.

I think we should standardize the spelling of "independent".

[Eric Wieser]

/poll Which token should we use for "independent"?

• Independent (rename SupIndep to SupIndependent etc)
• Indep (rename LinearIndependent to LinearIndep)
• The status quo is better than either option

[Martin Dvořák]

There is Matroid.Indep and IndepMatroid as well.

[Eric Wieser]

This looks like a slight majority towards LinearIndep; any further votes?

[Junyan Xu]

The abbreviation Lin is used in docs#Matrix.toLin, and the abbreviation Alg is used in docs#AlgHom and AlgEquiv, but not in docs#AlgebraicIndependent, docs#AlgebraCat, Subalgebra etc. Should we do LinIndep and AlgIndep?

[Kevin Buzzard]

And LinMap?

[Peter Nelson]

Projectivization.Independent is another data point.

[Violeta Hernández]

I vote against both Lin and Alg, they're abbreviations for much shorter words which aren't as obviously unambiguous.