Commit 2026-09-01 08:37 981fa8f5

View on Github →

feat: implement pi-base cross-reference attribute (#41487) Adds a @[pibase ID] cross-reference attribute for canonical pi-base identifiers. The parser accepts IDs of the form P000001, S000023, and T000001, and routes them to the corresponding properties/, spaces/, or theorems/ page on topology.pi-base.org. Tests cover docstring insertion, #pibase_tags, all three URL routes, and malformed IDs. This PR was prepared with assistance from Codex. Based heavily on #41290

Estimated changes

added theorem Pibase.p
added theorem Pibase.s
added theorem Pibase.t