feat(data/complex/exponential): add real.cos_abs (#13177)

leanprover-community · Apr 5, 2022 · cf131e1 · cf131e1
1 parent b011b0e
commit cf131e1
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
@@ -945,6 +945,9 @@ by rw [← of_real_inj]; simp [sin, sin_add]
 @[simp] lemma cos_neg : cos (-x) = cos x :=
 by simp [cos, exp_neg]
 
+@[simp] lemma cos_abs : cos (|x|) = cos x :=
+by cases le_total x 0; simp only [*, _root_.abs_of_nonneg, abs_of_nonpos, cos_neg]
+
 lemma cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
 by rw ← of_real_inj; simp [cos, cos_add]