diff options
| author | Michael Soegtrop | 2019-07-26 11:23:46 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2019-07-26 11:23:46 +0200 |
| commit | 2e37b4b30d0779dc960db80189e51ecd69f7e45a (patch) | |
| tree | f6583705ea010e8669388bc1af4af375a44c95b7 | |
| parent | 9b7b34702f1134841f7f9408db27074b5479e07d (diff) | |
| parent | 7865d0baf96ccbde37ed2f85e5ddbd5c24047eba (diff) | |
Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistency
Reviewed-by: MSoegtropIMC
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 5ed60b0a0f..2428fc495d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -178,7 +178,7 @@ Proof. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed. -Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. +Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. @@ -186,12 +186,16 @@ Proof. ring. Qed. -Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. +#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4. + +Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed. +#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4. + Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. apply Rsqr_inj... |