Commit 2026-03-24 04:38 1fb91738
View on Github →fix: mark projections @[reducible] around RelIso (#37032)
This PR continues the work of tagging manual projections between structures with reducible.
In particular, Equiv.toEmbedding, RelIso.toRelEmbedding and RelEmbedding.toRelHom.
I also removed the instance Equiv.Perm.coeEmbedding because it is superseded by Equiv.coeEmbedding.
I removed one set_option backward.isDefEq.respectTransparency, though presumably more can be removed after this.