Def Mathlib.CrossRef.Database.shortName

Modification history

2026-07-04 02:49
Mathlib/Tactic/CrossRefAttribute.lean
feat(scripts): export wikidata/stacks/kerodon cross-references as JSON (#40701) …
Added Mathlib.CrossRef.Database.shortNameView on Github →