(* Here I would prefer 'magma_op, but this breaks something in the next definition *)
interpretation "Left_coset" 'times x C =
(* Here I would prefer 'magma_op, but this breaks something in the next definition *)
interpretation "Left_coset" 'times x C =
definition member_of_left_coset ≝
λG:Group.λC:left_coset G.λx:G.
∃y.x=(element ? C)·y \sub (subgrp ? C).
interpretation "Member of left_coset" 'member_of x C =
definition member_of_left_coset ≝
λG:Group.λC:left_coset G.λx:G.
∃y.x=(element ? C)·y \sub (subgrp ? C).
interpretation "Member of left_coset" 'member_of x C =
(* The following should be a one-shot alias! *)
alias symbol "member_of" (instance 0) = "Member of subgroup".
(* The following should be a one-shot alias! *)
alias symbol "member_of" (instance 0) = "Member of subgroup".