Tautological action by relation automorphisms #
The tautological action by r →r r
on α
.
Equations
- RelHom.applyMulAction = { smul := DFunLike.coe, one_smul := ⋯, mul_smul := ⋯ }
The tautological action by r ↪r r
on α
.
Equations
- RelEmbedding.applyMulAction = { smul := DFunLike.coe, one_smul := ⋯, mul_smul := ⋯ }
The tautological action by r ≃r r
on α
.
Equations
- RelIso.applyMulAction = { smul := DFunLike.coe, one_smul := ⋯, mul_smul := ⋯ }