Commit 2024-09-19 16:02 1458edb5
View on Github →feat(RingTheory): composition of presentations (#16727)
Given an R-algebra S and an S-algebra T with presentations P and Q we construct the canonical R-presentation of T.
This contribution was created as part of the AIM workshop "Formalizing algebraic geometry"
in June 2024.