Loogle!

Result

Found 159 declarations mentioning Complex.sin.

• Complex.sin 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : ℂ
• Complex.ofReal_sin 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : ↑(Real.sin x) = Complex.sin ↑x
• Complex.sin_ofReal_re 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : (Complex.sin ↑x).re = Real.sin x
• Real.sin.eq_1 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : Real.sin x = (Complex.sin ↑x).re
• Complex.ofReal_sin_ofReal_re 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.sin ↑x).re = Complex.sin ↑x
• Complex.sin_neg 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin (-x) = -Complex.sin x
• Complex.sin_ofReal_im 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : (Complex.sin ↑x).im = 0
• Complex.sin_zero 📋 Mathlib.Data.Complex.Trigonometric
  : Complex.sin 0 = 0
• Complex.cot_eq_cos_div_sin 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : x.cot = Complex.cos x / Complex.sin x
• Complex.tan_eq_sin_div_cos 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.tan x = Complex.sin x / Complex.cos x
• Complex.cot.eq_1 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : z.cot = Complex.cos z / Complex.sin z
• Complex.tan.eq_1 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : Complex.tan z = Complex.sin z / Complex.cos z
• Complex.sin_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin (x * Complex.I) = Complex.sinh x * Complex.I
• Complex.sinh_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sinh (x * Complex.I) = Complex.sin x * Complex.I
• Complex.tan_mul_cos 📋 Mathlib.Data.Complex.Trigonometric
  {x : ℂ} (hx : Complex.cos x ≠ 0) : Complex.tan x * Complex.cos x = Complex.sin x
• Complex.cos_add_sin_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.cos x + Complex.sin x * Complex.I = Complex.exp (x * Complex.I)
• Complex.exp_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.exp (x * Complex.I) = Complex.cos x + Complex.sin x * Complex.I
• Complex.abs_cos_add_sin_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : ‖Complex.cos ↑x + Complex.sin ↑x * Complex.I‖ = 1
• Complex.norm_cos_add_sin_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℝ) : ‖Complex.cos ↑x + Complex.sin ↑x * Complex.I‖ = 1
• Complex.cos_sub_sin_I 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.cos x - Complex.sin x * Complex.I = Complex.exp (-x * Complex.I)
• Complex.exp_eq_exp_re_mul_sin_add_cos 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.exp x = Complex.exp ↑x.re * (Complex.cos ↑x.im + Complex.sin ↑x.im * Complex.I)
• Complex.cos_add 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.cos (x + y) = Complex.cos x * Complex.cos y - Complex.sin x * Complex.sin y
• Complex.cos_sub 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.cos (x - y) = Complex.cos x * Complex.cos y + Complex.sin x * Complex.sin y
• Complex.sin_add 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.sin (x + y) = Complex.sin x * Complex.cos y + Complex.cos x * Complex.sin y
• Complex.sin_sub 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.sin (x - y) = Complex.sin x * Complex.cos y - Complex.cos x * Complex.sin y
• Complex.cos_eq 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : Complex.cos z = Complex.cos ↑z.re * Complex.cosh ↑z.im - Complex.sin ↑z.re * Complex.sinh ↑z.im * Complex.I
• Complex.exp_add_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.exp (x + y * Complex.I) = Complex.exp x * (Complex.cos y + Complex.sin y * Complex.I)
• Complex.sin_eq 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : Complex.sin z = Complex.sin ↑z.re * Complex.cosh ↑z.im + Complex.cos ↑z.re * Complex.sinh ↑z.im * Complex.I
• Complex.sin_two_mul 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin (2 * x) = 2 * Complex.sin x * Complex.cos x
• Complex.cos_sq' 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.cos x ^ 2 = 1 - Complex.sin x ^ 2
• Complex.cos_sq_add_sin_sq 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.cos x ^ 2 + Complex.sin x ^ 2 = 1
• Complex.sin_sq 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin x ^ 2 = 1 - Complex.cos x ^ 2
• Complex.sin_sq_add_cos_sq 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin x ^ 2 + Complex.cos x ^ 2 = 1
• Complex.cos_add_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.cos (x + y * Complex.I) = Complex.cos x * Complex.cosh y - Complex.sin x * Complex.sinh y * Complex.I
• Complex.sin_add_mul_I 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.sin (x + y * Complex.I) = Complex.sin x * Complex.cosh y + Complex.cos x * Complex.sinh y * Complex.I
• Complex.sin.eq_1 📋 Mathlib.Data.Complex.Trigonometric
  (z : ℂ) : Complex.sin z = (Complex.exp (-z * Complex.I) - Complex.exp (z * Complex.I)) * Complex.I / 2
• Complex.two_sin 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : 2 * Complex.sin x = (Complex.exp (-x * Complex.I) - Complex.exp (x * Complex.I)) * Complex.I
• Complex.cos_two_mul' 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.cos (2 * x) = Complex.cos x ^ 2 - Complex.sin x ^ 2
• Complex.sin_conj 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.sin x)
• Complex.cos_add_sin_mul_I_pow 📋 Mathlib.Data.Complex.Trigonometric
  (n : ℕ) (z : ℂ) : (Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
• Complex.sin_three_mul 📋 Mathlib.Data.Complex.Trigonometric
  (x : ℂ) : Complex.sin (3 * x) = 3 * Complex.sin x - 4 * Complex.sin x ^ 3
• Complex.tan_sq_div_one_add_tan_sq 📋 Mathlib.Data.Complex.Trigonometric
  {x : ℂ} (hx : Complex.cos x ≠ 0) : Complex.tan x ^ 2 / (1 + Complex.tan x ^ 2) = Complex.sin x ^ 2
• Complex.sin_add_sin 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.sin x + Complex.sin y = 2 * Complex.sin ((x + y) / 2) * Complex.cos ((x - y) / 2)
• Complex.sin_sub_sin 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.sin x - Complex.sin y = 2 * Complex.sin ((x - y) / 2) * Complex.cos ((x + y) / 2)
• Complex.cos_sub_cos 📋 Mathlib.Data.Complex.Trigonometric
  (x y : ℂ) : Complex.cos x - Complex.cos y = -2 * Complex.sin ((x + y) / 2) * Complex.sin ((x - y) / 2)
• Complex.sin_antiperiodic 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Function.Antiperiodic Complex.sin ↑Real.pi
• Complex.sin_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Complex.sin ↑Real.pi = 0
• Complex.sin_pi_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (↑Real.pi - x) = Complex.sin x
• Complex.sin_add_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x + ↑Real.pi) = -Complex.sin x
• Complex.sin_sub_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x - ↑Real.pi) = -Complex.sin x
• Complex.sin_int_mul_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (n : ℤ) : Complex.sin (↑n * ↑Real.pi) = 0
• Complex.sin_nat_mul_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (n : ℕ) : Complex.sin (↑n * ↑Real.pi) = 0
• Complex.sin_periodic 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Function.Periodic Complex.sin (2 * ↑Real.pi)
• Complex.continuous_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Continuous Complex.sin
• Complex.sin_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Complex.sin (2 * ↑Real.pi) = 0
• Complex.continuousOn_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  {s : Set ℂ} : ContinuousOn Complex.sin s
• Complex.sin_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : Complex.sin (↑Real.pi / 2) = 1
• Complex.cos_eq_zero_iff_sin_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  {z : ℂ} : Complex.cos z = 0 ↔ Complex.sin z = 1 ∨ Complex.sin z = -1
• Complex.sin_add_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x + 2 * ↑Real.pi) = Complex.sin x
• Complex.sin_eq_zero_iff_cos_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  {z : ℂ} : Complex.sin z = 0 ↔ Complex.cos z = 1 ∨ Complex.cos z = -1
• Complex.sin_sub_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x - 2 * ↑Real.pi) = Complex.sin x
• Complex.cos_pi_div_two_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.cos (↑Real.pi / 2 - x) = Complex.sin x
• Complex.cos_sub_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.cos (x - ↑Real.pi / 2) = Complex.sin x
• Complex.sin_add_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x + ↑Real.pi / 2) = Complex.cos x
• Complex.sin_pi_div_two_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (↑Real.pi / 2 - x) = Complex.cos x
• Complex.sin_two_pi_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (2 * ↑Real.pi - x) = -Complex.sin x
• Complex.cos_add_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.cos (x + ↑Real.pi / 2) = -Complex.sin x
• Complex.sin_sub_pi_div_two 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) : Complex.sin (x - ↑Real.pi / 2) = -Complex.cos x
• Complex.sin_add_int_mul_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℤ) : Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x
• Complex.sin_add_nat_mul_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℕ) : Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x
• Complex.sin_sub_int_mul_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℤ) : Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
• Complex.sin_sub_nat_mul_two_pi 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℕ) : Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
• Complex.sin_int_mul_two_pi_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℤ) : Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
• Complex.sin_nat_mul_two_pi_sub 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  (x : ℂ) (n : ℕ) : Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
• Complex.abs_mul_cos_add_sin_mul_I 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  (x : ℂ) : ↑‖x‖ * (Complex.cos ↑x.arg + Complex.sin ↑x.arg * Complex.I) = x
• Complex.norm_mul_cos_add_sin_mul_I 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  (x : ℂ) : ↑‖x‖ * (Complex.cos ↑x.arg + Complex.sin ↑x.arg * Complex.I) = x
• Complex.arg_cos_add_sin_mul_I 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = θ
• Complex.arg_cos_add_sin_mul_I_eq_toIocMod 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  (θ : ℝ) : (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
• Complex.arg_mul_cos_add_sin_mul_I 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = θ
• Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {r : ℝ} (hr : 0 < r) (θ : ℝ) : (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
• Complex.arg_cos_add_sin_mul_I_sub 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  (θ : ℝ) : (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋
• Complex.arg_mul_cos_add_sin_mul_I_sub 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {r : ℝ} (hr : 0 < r) (θ : ℝ) : (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋
• Complex.measurable_sin 📋 Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
  : Measurable Complex.sin
• Measurable.csin 📋 Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
  {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ} (hf : Measurable f) : Measurable fun x => Complex.sin (f x)
• AEMeasurable.csin 📋 Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : AEMeasurable f μ) : AEMeasurable (fun x => Complex.sin (f x)) μ
• Complex.logDeriv_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  : logDeriv Complex.sin = Complex.cot
• Complex.analyticAt_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {x : ℂ} : AnalyticAt ℂ Complex.sin x
• Complex.analyticOnNhd_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {s : Set ℂ} : AnalyticOnNhd ℂ Complex.sin s
• Complex.analyticOn_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {s : Set ℂ} : AnalyticOn ℂ Complex.sin s
• Complex.contDiff_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {n : WithTop ℕ∞} : ContDiff ℂ n Complex.sin
• Complex.analyticWithinAt_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {x : ℂ} {s : Set ℂ} : AnalyticWithinAt ℂ Complex.sin s x
• Complex.deriv_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  : deriv Complex.sin = Complex.cos
• Complex.deriv_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {x : ℂ} : deriv Complex.cos x = -Complex.sin x
• Complex.deriv_cos' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  : deriv Complex.cos = fun x => -Complex.sin x
• ContDiff.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {n : WithTop ℕ∞} (h : ContDiff ℂ n f) : ContDiff ℂ n fun x => Complex.sin (f x)
• ContDiffAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞} (hf : ContDiffAt ℂ n f x) : ContDiffAt ℂ n (fun x => Complex.sin (f x)) x
• ContDiffOn.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffOn ℂ n f s) : ContDiffOn ℂ n (fun x => Complex.sin (f x)) s
• ContDiffWithinAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℂ n f s x) : ContDiffWithinAt ℂ n (fun x => Complex.sin (f x)) s x
• Complex.differentiable_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  : Differentiable ℂ Complex.sin
• Complex.differentiableAt_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {x : ℂ} : DifferentiableAt ℂ Complex.sin x
• Differentiable.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hc : Differentiable ℂ f) : Differentiable ℂ fun x => Complex.sin (f x)
• DifferentiableAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) : DifferentiableAt ℂ (fun x => Complex.sin (f x)) x
• DifferentiableOn.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (hc : DifferentiableOn ℂ f s) : DifferentiableOn ℂ (fun x => Complex.sin (f x)) s
• DifferentiableWithinAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℂ f s x) : DifferentiableWithinAt ℂ (fun x => Complex.sin (f x)) s x
• Complex.hasDerivAt_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (x : ℂ) : HasDerivAt Complex.sin (Complex.cos x) x
• Complex.hasStrictDerivAt_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (x : ℂ) : HasStrictDerivAt Complex.sin (Complex.cos x) x
• deriv_csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {x : ℂ} (hc : DifferentiableAt ℂ f x) : deriv (fun x => Complex.sin (f x)) x = Complex.cos (f x) * deriv f x
• Complex.hasDerivAt_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (x : ℂ) : HasDerivAt Complex.cos (-Complex.sin x) x
• Complex.hasStrictDerivAt_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (x : ℂ) : HasStrictDerivAt Complex.cos (-Complex.sin x) x
• deriv_ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {x : ℂ} (hc : DifferentiableAt ℂ f x) : deriv (fun x => Complex.cos (f x)) x = -Complex.sin (f x) * deriv f x
• derivWithin_csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ} (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) : derivWithin (fun x => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x
• derivWithin_ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ} (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) : derivWithin (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x
• HasDerivAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
• HasStrictDerivAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
• HasDerivAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
• HasStrictDerivAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
• HasDerivWithinAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') s x
• HasDerivWithinAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ} (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') s x
• fderiv_csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) : fderiv ℂ (fun x => Complex.sin (f x)) x = Complex.cos (f x) • fderiv ℂ f x
• fderiv_ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) : fderiv ℂ (fun x => Complex.cos (f x)) x = -Complex.sin (f x) • fderiv ℂ f x
• fderivWithin_csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) : fderivWithin ℂ (fun x => Complex.sin (f x)) s x = Complex.cos (f x) • fderivWithin ℂ f s x
• fderivWithin_ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℂ f s x) (hxs : UniqueDiffWithinAt ℂ s x) : fderivWithin ℂ (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) • fderivWithin ℂ f s x
• HasFDerivAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
• HasStrictFDerivAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
• HasFDerivAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
• HasStrictFDerivAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
• HasFDerivWithinAt.csin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') s x
• HasFDerivWithinAt.ccos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') s x
• Complex.sin_surjective 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  : Function.Surjective Complex.sin
• Complex.range_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  : Set.range Complex.sin = Set.univ
• Complex.sin_ne_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  {θ : ℂ} : Complex.sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑Real.pi
• Complex.sin_eq_zero_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  {θ : ℂ} : Complex.sin θ = 0 ↔ ∃ k, θ = ↑k * ↑Real.pi
• Complex.sin_eq_one_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  {x : ℂ} : Complex.sin x = 1 ↔ ∃ k, ↑Real.pi / 2 + ↑k * (2 * ↑Real.pi) = x
• Complex.sin_eq_neg_one_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  {x : ℂ} : Complex.sin x = -1 ↔ ∃ k, -(↑Real.pi / 2) + ↑k * (2 * ↑Real.pi) = x
• Complex.sin_eq_sin_iff 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
  {x y : ℂ} : Complex.sin x = Complex.sin y ↔ ∃ k, y = 2 * ↑k * ↑Real.pi + x ∨ y = (2 * ↑k + 1) * ↑Real.pi - x
• integral_cos_mul_complex 📋 Mathlib.Analysis.SpecialFunctions.Integrals.Basic
  {z : ℂ} (hz : z ≠ 0) (a b : ℝ) : ∫ (x : ℝ) in a..b, Complex.cos (z * ↑x) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z
• Complex.tendsto_euler_sin_prod 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  (z : ℂ) : Filter.Tendsto (fun n => ↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) Filter.atTop (nhds (Complex.sin (↑Real.pi * z)))
• EulerSine.integral_cos_mul_cos_pow_aux 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  {z : ℂ} {n : ℕ} (hn : 2 ≤ n) (hz : z ≠ 0) : ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n = ↑n / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1)
• EulerSine.antideriv_cos_comp_const_mul 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  {z : ℂ} (hz : z ≠ 0) (x : ℝ) : HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
• EulerSine.antideriv_sin_comp_const_mul 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  {z : ℂ} (hz : z ≠ 0) (x : ℝ) : HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
• EulerSine.sin_pi_mul_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  (z : ℂ) (n : ℕ) : Complex.sin (↑Real.pi * z) = ((↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ (2 * n))
• EulerSine.integral_sin_mul_sin_mul_cos_pow_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  {z : ℂ} {n : ℕ} (hn : 2 ≤ n) (hz : z ≠ 0) : ∫ (x : ℝ) in 0..Real.pi / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1) = (↑n / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n) - (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)
• Complex.Gamma_mul_Gamma_one_sub 📋 Mathlib.Analysis.SpecialFunctions.Gamma.Beta
  (z : ℂ) : Complex.Gamma z * Complex.Gamma (1 - z) = ↑Real.pi / Complex.sin (↑Real.pi * z)
• Complex.hasSum_sin' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I) (Complex.sin z)
• Complex.sin_eq_tsum' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I
• Complex.hasSum_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Complex.sin z)
• Complex.sin_eq_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
• Complex.inv_Gammaℝ_two_sub 📋 Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
  {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) : (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑Real.pi * s / 2) * (s + 1).Gammaℝ⁻¹
• Polynomial.Chebyshev.U_complex_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
  (θ : ℂ) (n : ℤ) : Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.U ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)
• Polynomial.Chebyshev.S_two_mul_complex_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
  (θ : ℂ) (n : ℤ) : Polynomial.eval (2 * Complex.cos θ) (Polynomial.Chebyshev.S ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)
• sin_pi_z_ne_zero 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hz : x ∈ Complex.integerComplement) : Complex.sin (↑Real.pi * x) ≠ 0
• euler_sineTerm_tprod 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hx : x ∈ Complex.integerComplement) : ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin (↑Real.pi * x) / (↑Real.pi * x)
• HasProdLocallyUniformlyOn_euler_sin_prod 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  : HasProdLocallyUniformlyOn (fun n z => 1 + sineTerm z n) (fun x => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) Complex.integerComplement
• tendsto_euler_sin_prod' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (h0 : x ≠ 0) : Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, (1 + sineTerm x i)) Filter.atTop (nhds (Complex.sin (↑Real.pi * x) / (↑Real.pi * x)))
• HasProdUniformlyOn_sineTerm_prod_on_compact 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {Z : Set ℂ} (hZ2 : Z ⊆ Complex.integerComplement) (hZC : IsCompact Z) : HasProdUniformlyOn (fun n z => 1 + sineTerm z n) (fun x => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) {Z}
• logDeriv_sin_div_eq_cot 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hz : x ∈ Complex.integerComplement) : logDeriv (fun t => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x = ↑Real.pi * (↑Real.pi * x).cot - 1 / x
• tendsto_logDeriv_euler_sin_div 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hx : x ∈ Complex.integerComplement) : Filter.Tendsto (fun n => logDeriv (fun z => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) Filter.atTop (nhds (logDeriv (fun t => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x))
• HurwitzZeta.hurwitzZetaOdd_one_sub 📋 Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
  (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) : HurwitzZeta.hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.sinZeta a s
• HurwitzZeta.sinZeta_one_sub 📋 Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
  (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) : HurwitzZeta.sinZeta a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.hurwitzZetaOdd a s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 06e7f72 serving mathlib revision e128198