diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-20 10:42:41 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-20 10:42:41 -0400 |
| commit | e759d1fee38ec02d3744a9322a1cf7bff1f4ab28 (patch) | |
| tree | 3d294f5fbba266d1a15f6641984c5f90f51ef5ac /src/Algebra.v | |
| parent | 0ec7bb713a5ab9af36432bde96756536b8efb820 (diff) | |
More missing scopes for 8.5?
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index cafafe7d3..b8cc3c921 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -143,6 +143,8 @@ Module Monoid. Context {T eq op id} {monoid:@monoid T eq op id}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "*" := op. + Local Infix "=" := eq : eq_scope. + Local Open Scope eq_scope. Lemma cancel_right z iz (Hinv:op z iz = id) : forall x y, x * z = y * z <-> x = y. @@ -195,6 +197,8 @@ Module Group. Context {T eq op id inv} `{@group T eq op id inv}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "*" := op. + Local Infix "=" := eq : eq_scope. + Local Open Scope eq_scope. Lemma cancel_left : forall z x y, z*x = z*y <-> x = y. Proof. eauto using Monoid.cancel_left, left_inverse. Qed. |