chore(analysis/special_functions/trigonometric/angle): rfl lemmas for…

… nat and int smul actions on angle (#15003) These can't be simp, because the simp-normal form is multiplication.
leanprover-community · Jun 28, 2022 · cf4d987 · cf4d987
1 parent 37bf8a2
commit cf4d987
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/analysis/special_functions/trigonometric/angle.lean b/src/analysis/special_functions/trigonometric/angle.lean
@@ -47,6 +47,8 @@ quotient.induction_on' θ h
 @[simp] lemma coe_add (x y : ℝ) : ↑(x + y : ℝ) = (↑x + ↑y : angle) := rfl
 @[simp] lemma coe_neg (x : ℝ) : ↑(-x : ℝ) = -(↑x : angle) := rfl
 @[simp] lemma coe_sub (x y : ℝ) : ↑(x - y : ℝ) = (↑x - ↑y : angle) := rfl
+lemma coe_nsmul (n : ℕ) (x : ℝ) : ↑(n • x : ℝ) = (n • ↑x : angle) := rfl
+lemma coe_zsmul (z : ℤ) (x : ℝ) : ↑(z • x : ℝ) = (z • ↑x : angle) := rfl
 
 @[simp, norm_cast] lemma coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
   ↑((n : ℝ) * x) = n • (↑x : angle) :=