Relation isomorphisms form a group #
Equations
- RelHom.instMonoid = { mul := RelHom.comp, mul_assoc := ⋯, one := RelHom.id r, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }
Equations
- RelEmbedding.instMonoid = { mul := fun (f g : r ↪r r) => g.trans f, mul_assoc := ⋯, one := RelEmbedding.refl r, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }