feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lem…

…mas (#11482)

Add some more lemmas useful for manipulation of `real.angle` expressions.

src/analysis/special_functions/trigonometric/angle.lean

@@ -63,6 +63,15 @@ begin
   simp [two_mul, sub_eq_add_neg]
 end
 
+lemma sub_coe_pi_eq_add_coe_pi (θ : angle) : θ - π = θ + π :=
+by rw [sub_eq_add_neg, neg_coe_pi]
+
+@[simp] lemma two_nsmul_coe_pi : (2 : ℕ) • (π : angle) = 0 :=
+by simp [←coe_nat_mul_eq_nsmul]
+
+@[simp] lemma two_zsmul_coe_pi : (2 : ℤ) • (π : angle) = 0 :=
+by simp [←coe_int_mul_eq_zsmul]
+
 theorem cos_eq_iff_eq_or_eq_neg {θ ψ : ℝ} : cos θ = cos ψ ↔ (θ : angle) = ψ ∨ (θ : angle) = -ψ :=
 begin
   split,