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

The tautological action by r ≃r r on α.

Equations

• RelIso.applyMulAction = MulAction.mk ⋯ ⋯

instance RelIso.applyOpMulAction {α : Type u_1} {r : α → α → Prop} : MulAction (r ≃r r)ᵐᵒᵖ α

The tautological action by r ≃r r on α.

Equations

• RelIso.applyOpMulAction = MulAction.mk ⋯ ⋯

@[simp]

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

@[simp]

theorem RelIso.op_smul_def {α : Type u_1} {r : α → α → Prop} (f : (r ≃r r)ᵐᵒᵖ) (a : α) : f • a = (MulOpposite.unop f).symm a

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

instance RelIso.apply_op_faithfulSMul {α : Type u_1} {r : α → α → Prop} : FaithfulSMul (r ≃r r)ᵐᵒᵖ α