Tautological action by relation automorphisms

@[instance_reducible]

instance RelHom.applyMulAction {α : Type u_1} {r : α → α → Prop} : MulAction (r →r r) α

The tautological action by r →r r on α.

Equations

• RelHom.applyMulAction = { smul := DFunLike.coe, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem RelHom.smul_def {α : Type u_1} {r : α → α → Prop} (f : r →r r) (a : α) : f • a = f a

instance RelHom.apply_faithfulSMul {α : Type u_1} {r : α → α → Prop} : FaithfulSMul (r →r r) α

@[instance_reducible]

instance RelEmbedding.applyMulAction {α : Type u_1} {r : α → α → Prop} : MulAction (r ↪r r) α

The tautological action by r ↪r r on α.

Equations

• RelEmbedding.applyMulAction = { smul := DFunLike.coe, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem RelEmbedding.smul_def {α : Type u_1} {r : α → α → Prop} (f : r ↪r r) (a : α) : f • a = f a

instance RelEmbedding.apply_faithfulSMul {α : Type u_1} {r : α → α → Prop} : FaithfulSMul (r ↪r r) α

@[instance_reducible]

instance RelIso.applyMulAction {α : Type u_1} {r : α → α → Prop} : MulAction (r ≃r r) α

The tautological action by r ≃r r on α.

Equations

• RelIso.applyMulAction = { smul := DFunLike.coe, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem RelIso.smul_def {α : Type u_1} {r : α → α → Prop} (f : r ≃r r) (a : α) : f • a = f a

instance RelIso.apply_faithfulSMul {α : Type u_1} {r : α → α → Prop} : FaithfulSMul (r ≃r r) α