- { is_monoid:> isMonoid G;
- inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
- inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
+ { is_monoid :> IsMonoid G;
+ inv_is_left_inverse : is_left_inverse G (inv G);
+ inv_is_right_inverse: is_right_inverse G (inv G)
rewrite < (e_is_left_unit ? G);
rewrite < (e_is_left_unit ? G z);
rewrite < (inv_is_left_inverse ? G x);
rewrite < (e_is_left_unit ? G);
rewrite < (e_is_left_unit ? G z);
rewrite < (inv_is_left_inverse ? G x);
theorem eq_op_x_y_op_z_y_to_eq:
∀G:Group. right_cancellable G (op G).
intros;
unfold right_cancellable;
unfold injective;
theorem eq_op_x_y_op_z_y_to_eq:
∀G:Group. right_cancellable G (op G).
intros;
unfold right_cancellable;
unfold injective;
intros (x y z);
rewrite < (e_is_right_unit ? G);
rewrite < (e_is_right_unit ? G z);
rewrite < (inv_is_right_inverse ? G x);
intros (x y z);
rewrite < (e_is_right_unit ? G);
rewrite < (e_is_right_unit ? G z);
rewrite < (inv_is_right_inverse ? G x);
∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
rewrite > (inv_is_left_inverse ? G);
rewrite > (e_is_right_unit ? G);
rewrite > (inv_is_left_inverse ? G);
rewrite > (inv_is_left_inverse ? G);
rewrite > (e_is_right_unit ? G);
rewrite > (inv_is_left_inverse ? G);
(* 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".
rewrite > (inv_is_left_inverse ? G);
rewrite > (e_is_left_unit ? G);
rewrite < (f_morph ? ? H);
rewrite > (inv_is_left_inverse ? G);
rewrite > (e_is_left_unit ? G);
rewrite < (f_morph ? ? H);