diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-10 15:29:49 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-10 15:31:19 -0400 |
| commit | 2b7ee7e329e50c39c99d9c17756d6f8ff1a021ae (patch) | |
| tree | ebfbcd73b59fdf87313bbcf30a88fa345175ba80 /src/Algebra.v | |
| parent | 64cca72b6d3aec937ecd51bd2a26549b94389bd3 (diff) | |
Added helper lemma to Algebra.
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 8c4c472cc..9db169816 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -714,6 +714,12 @@ Module Field. apply zero_neq_one. assumption. Qed. + Lemma div_one x : div x one = x. + Proof. + rewrite field_div_definition. + rewrite <-(inv_unique 1 1); apply monoid_is_right_identity. + Qed. + Lemma mul_cancel_l_iff : forall x y, y <> 0 -> (x * y = y <-> x = one). Proof. |