Tag queue

Pending @[wikidata] tags for the next Mathlib batch. updated 2026-06-23T20:07:27.712Z

Recycled — needs a retarget 5

↻ recycled Q269878 big O notation
↳ retarget: I don't think this is the appropriate Wikidata tag. Asymptotic Analysis is a field of math, we want the entry specifically for "Big O"
↻ recycled Q189569 basisBasis
↳ retarget: Basis — This does not cover polar/spherical/hyperbolic coordinate systems as discussed in the Wikipedia article. "Coordinate system" is a much more general concept. Instead, we should tag `Basis` with Q189569
↻ recycled Q752487 dual spaceDual
↳ retarget: Dual — Duality is a more general concept. We should instead tag `Dual` with Q752487 (Dual Space)
↻ recycled Q833293 trapezoidal ruletrapezoidal_integral
↳ retarget: trapezoidal_integral — Numerical integration is a more general concept. We should instead tag `trapezoidal_integral` with Q833293 (trapezoidal rule)
↻ recycled Q605807 Erdős–Rényi model
↳ retarget: "Random graph" is too broad. We should instead tag with Q605807 (Erdős–Rényi model) since this is the `G(V,p)` model described by `binomialRandom`. See: https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%

Unreviewed candidates 20

◷ unreviewed Q467606 model theoryFirstOrder.Language.Theory.Model
◷ unreviewed Q50698 algebraic equationPolynomial.IsRoot
◷ unreviewed Q382698 affine spaceAffineSpace
◷ unreviewed Q7874246 Coxeter groupIsCoxeterGroup
◷ unreviewed Q600590 𝑛-tupleFin.cons
◷ unreviewed Q181365 scalar productMatrix.dotProduct
◷ unreviewed Q524607 general linear groupMatrix.GeneralLinearGroup
◷ unreviewed Q50695 quadratic functiondiscrim
◷ unreviewed Q602136 coding theoryUniquelyDecodable
◷ unreviewed Q255166 Kullback–Leibler divergenceklDiv
◷ unreviewed Q192161 formal languageLanguage
◷ unreviewed Q1378376 line graphSimpleGraph.lineGraph
◷ unreviewed Q226183 empty setSet.instEmptyCollection
◷ unreviewed Q1196523 implicit functionImplicitFunctionData.implicitFunction
◷ unreviewed Q1046291 topological groupIsTopologicalGroup
◷ unreviewed Q93344 trigonometric functionReal.sin
◷ unreviewed Q12507 sphereMetric.sphere
◷ unreviewed Q1049914 matrix multiplicationMatrix.mul_apply
◷ unreviewed Q230967 parityEven
◷ unreviewed Q117806 gamma distributiongammaMeasure