Getting a list of all mathlib theorems fully-namespaced

Stream: mathlib4

[Bolton Bailey]

Working in /Data, I often notice things that are present in only one of the Polynomial and MvPolynomial namespaces, but should be present in both. The same goes for Finset Multiset and List.

I'd like to investigate this a bit more rigorously. Is there some way to get a list of all the lemmas in mathlib so I can see if there are other namespaces that overlap and which lemmas from other namespaces overlap with which others?

[Floris van Doorn]

Something like this?

import Mathlib.Lean.Expr.Basic

open Lean

run_cmd do
  -- all constants in imported files
  let constants := (← getEnv).constants.map₁.toList.map (·.1)
  -- remove some auto-generated constants
  let constants ← constants.filterM fun nm ↦ return !(← nm.isBlackListed)
  -- print first 100
  logInfo m!"{constants |>.take 100}"

[Bolton Bailey]

That works perfectly, thanks!

[Bolton Bailey]

For Zulip's viewing pleasure: the top 100 most similar namespace pairs by intersection-over-union (out of namespaces with at least 200 declarations).

IOU: 0.51 Subring Subsemiring
IOU: 0.41 WithTop WithBot
IOU: 0.39 AddMonoidHom MonoidHom
IOU: 0.39 Subgroup AddSubgroup
IOU: 0.38 AddSubmonoid Submonoid
IOU: 0.26 Finsupp DFinsupp
IOU: 0.24 Submonoid Subsemiring
IOU: 0.23 Submonoid Subring
IOU: 0.23 AddSubgroup AddSubmonoid
IOU: 0.22 AddSubmonoid Subring
IOU: 0.22 AddSubmonoid Subsemiring
IOU: 0.22 Subgroup Submonoid
IOU: 0.21 AddEquiv RingEquiv
IOU: 0.20 ULift MulOpposite
IOU: 0.20 Subalgebra Subsemiring
IOU: 0.20 Filter.Germ Function.Injective
IOU: 0.20 Subalgebra Subring
IOU: 0.19 AlgEquiv RingEquiv
IOU: 0.19 AddSubgroup Submonoid
IOU: 0.18 Subgroup AddSubmonoid
IOU: 0.17 MonoidHom RingHom
IOU: 0.17 AddMonoidHom RingHom
IOU: 0.17 Function.Injective MulOpposite
IOU: 0.17 AlgEquiv AddEquiv
IOU: 0.16 RingHom AlgHom
IOU: 0.16 Filter.Germ MulOpposite
IOU: 0.15 ULift Filter.Germ
IOU: 0.15 ULift Function.Injective
IOU: 0.15 Subgroup Subring
IOU: 0.15 AlgEquiv AlgHom
IOU: 0.15 IntermediateField Subalgebra
IOU: 0.15 AddSubgroup Subring
IOU: 0.14 AddSubgroup Subsemiring
IOU: 0.14 Filter.Tendsto Continuous
IOU: 0.14 Subgroup Subsemiring
IOU: 0.14 LinearEquiv AddEquiv
IOU: 0.13 LinearEquiv RingEquiv
IOU: 0.13 ENNReal NNReal
IOU: 0.13 Pi ULift
IOU: 0.13 LinearEquiv AlgEquiv
IOU: 0.13 Pi Function.Injective
IOU: 0.13 Pi Prod
IOU: 0.13 Nat Int
IOU: 0.12 LinearEquiv ContinuousLinearEquiv
IOU: 0.11 Pi Filter.Germ
IOU: 0.11 Set Finset
IOU: 0.10 OrderIso Homeomorph
IOU: 0.10 MonoidHom AlgHom
IOU: 0.10 Complex IsROrC
IOU: 0.10 Real Complex
IOU: 0.10 Submodule AddSubmonoid
IOU: 0.10 Pi MulOpposite
IOU: 0.10 IntermediateField Subring
IOU: 0.10 AddMonoidHom AlgHom
IOU: 0.09 Submonoid Subalgebra
IOU: 0.09 WithTop EReal
IOU: 0.09 ContinuousMap BoundedContinuousFunction
IOU: 0.09 IntermediateField Subsemiring
IOU: 0.09 Homeomorph ContinuousLinearEquiv
IOU: 0.08 WithBot EReal
IOU: 0.08 WithTop Filter.Germ
IOU: 0.08 AddSubmonoid Subalgebra
IOU: 0.08 ContinuousLinearMap ContinuousMultilinearMap
IOU: 0.08 LinearMap ContinuousLinearMap
IOU: 0.08 Finset Multiset
IOU: 0.08 RingEquiv AlgHom
IOU: 0.08 LinearEquiv Homeomorph
IOU: 0.08 ContinuousLinearEquiv AddEquiv
IOU: 0.08 LinearMap AddMonoidHom
IOU: 0.08 Equiv Homeomorph
IOU: 0.08 MulOpposite TrivSqZeroExt
IOU: 0.08 WithBot Filter.Germ
IOU: 0.08 Submodule AddSubgroup
IOU: 0.08 List Multiset
IOU: 0.07 Filter.Germ TrivSqZeroExt
IOU: 0.07 ULift TrivSqZeroExt
IOU: 0.07 Prod ULift
IOU: 0.07 CategoryTheory.ShortComplex HomologicalComplex
IOU: 0.07 RingHom RingEquiv
IOU: 0.07 Submodule Submonoid
IOU: 0.07 AddMonoidHom AddEquiv
IOU: 0.07 Homeomorph AddEquiv
IOU: 0.07 AddSubgroup Subalgebra
IOU: 0.07 ENNReal WithTop
IOU: 0.07 LieSubmodule Subring
IOU: 0.07 ContinuousLinearMap AddMonoidHom
IOU: 0.07 Equiv OrderIso
IOU: 0.07 AffineSubspace LieSubmodule
IOU: 0.07 LieSubmodule Subsemiring
IOU: 0.07 RingHom AlgEquiv
IOU: 0.06 AffineSubspace Subring
IOU: 0.06 AffineSubspace Subsemiring
IOU: 0.06 AddSubmonoid LieSubmodule
IOU: 0.06 Homeomorph RingEquiv
IOU: 0.06 Option Part
IOU: 0.06 AlgEquiv ContinuousLinearEquiv
IOU: 0.06 ContinuousLinearEquiv RingEquiv
IOU: 0.06 Pi DFinsupp
IOU: 0.06 Subgroup Subalgebra
IOU: 0.06 Equiv LinearEquiv

[Johan Commelin]

"Similar" means "contain many lemmas with the same name"? Or what exactly?

[Bolton Bailey]

It just means that a large fraction of lemma names that appear in one appear in both.