feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul#38172

joelriou wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

joelriou:relstruct-equiv-mulstructjoelriou/mathlib4:relstruct-equiv-mulstructCopy head branch name to clipboard