Formalizing multi-graded Brenner-Schr"oer Proj schemes and dilatations of rings in Lean4
Not on the map. Why?
Abstract (arXiv)
We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schr"oer Proj construction and algebraic dilatations of rings.
Key facts. Cited by 2 papers in the map (data through 14 Oct 2026). First posted on arXiv 31 May 2026.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2026: 2.
2 papers.