Commit 2026-02-20 16:02 0b16e4ae
View on Github →chore(CategoryTheory/Triangulated): remove someOctahedron' (#35501)
The now duplicate definition someOctahedron' is removed. (The reason for its existence is related to some bug which occurred at the time of the port to Lean 3 #3072.)
(No deprecated alias is added as it was only part of the implementation of someOctahedron, and we may want to reuse the name for #35496.)