Feedback on the Current Page
Arend Mellendijk. algebra-tactic (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
@misc{dagstuhl-artifact-27124,
title = {{algebra-tactic}},
author = {Mellendijk, Arend},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:c939acdbc385233836c284ca55f264661c444c36;origin=https://github.com/amellendijk/algebra-tactic;visit=swh:1:snp:1ae7b2d2024fcbb577fe915ce6e3e8268ea25d74;anchor=swh:1:rev:3372ce1dc459f56e8de10abdfd51f3deaa4b0411}{\texttt{swh:1:dir:c939acdbc385233836c284ca55f264661c444c36}} (visited on 2026-07-16)},
url = {https://github.com/amellendijk/algebra-tactic},
doi = {10.4230/artifacts.27124},
}
Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)
Arend Mellendijk. A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
@InProceedings{mellendijk:LIPIcs.ITP.2026.35,
author = {Mellendijk, Arend},
title = {{A Lean Tactic for Normalizing Expressions in an Algebra over a Ring}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {35:1--35:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.35},
URN = {urn:nbn:de:0030-drops-270099},
doi = {10.4230/LIPIcs.ITP.2026.35},
annote = {Keywords: Lean, Mathlib, algebraic structures, proof algorithms}
}