Loogle!

Result

Found 461 declarations whose name contains "ofReal". Of these, 159 have a name containing "Complex." and "ofReal".

• Complex.ofReal 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : ℂ
• Complex.ofReal_injective 📋 Mathlib.Data.Complex.Basic
  : Function.Injective Complex.ofReal
• Complex.ofReal_re 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : (↑r).re = r
• Complex.ofRealHom 📋 Mathlib.Data.Complex.Basic
  : ℝ →+* ℂ
• Complex.ofReal_im 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : (↑r).im = 0
• Complex.ofReal_intCast 📋 Mathlib.Data.Complex.Basic
  (n : ℤ) : ↑↑n = ↑n
• Complex.ofReal_natCast 📋 Mathlib.Data.Complex.Basic
  (n : ℕ) : ↑↑n = ↑n
• Complex.ofReal_nnratCast 📋 Mathlib.Data.Complex.Basic
  (q : ℚ≥0) : ↑↑q = ↑q
• Complex.ofReal_ratCast 📋 Mathlib.Data.Complex.Basic
  (q : ℚ) : ↑↑q = ↑q
• Complex.ofReal_def 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : ↑r = { re := r, im := 0 }
• Complex.ofReal_inj 📋 Mathlib.Data.Complex.Basic
  {z w : ℝ} : ↑z = ↑w ↔ z = w
• Complex.ofReal_inv 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : ↑r⁻¹ = (↑r)⁻¹
• Complex.ofReal_neg 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : ↑(-r) = -↑r
• Complex.ofReal.eq_1 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : ↑r = { re := r, im := 0 }
• Complex.ofReal_one 📋 Mathlib.Data.Complex.Basic
  : ↑1 = 1
• Complex.ofReal_zero 📋 Mathlib.Data.Complex.Basic
  : ↑0 = 0
• Complex.ofReal_eq_one 📋 Mathlib.Data.Complex.Basic
  {z : ℝ} : ↑z = 1 ↔ z = 1
• Complex.ofReal_eq_zero 📋 Mathlib.Data.Complex.Basic
  {z : ℝ} : ↑z = 0 ↔ z = 0
• Complex.ofReal_ne_one 📋 Mathlib.Data.Complex.Basic
  {z : ℝ} : ↑z ≠ 1 ↔ z ≠ 1
• Complex.ofReal_ne_zero 📋 Mathlib.Data.Complex.Basic
  {z : ℝ} : ↑z ≠ 0 ↔ z ≠ 0
• Complex.ofReal_ofNat 📋 Mathlib.Data.Complex.Basic
  (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n
• Complex.im_mul_ofReal 📋 Mathlib.Data.Complex.Basic
  (z : ℂ) (r : ℝ) : (z * ↑r).im = z.im * r
• Complex.im_ofReal_mul 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im
• Complex.ofReal_add 📋 Mathlib.Data.Complex.Basic
  (r s : ℝ) : ↑(r + s) = ↑r + ↑s
• Complex.ofReal_mul 📋 Mathlib.Data.Complex.Basic
  (r s : ℝ) : ↑(r * s) = ↑r * ↑s
• Complex.ofReal_sub 📋 Mathlib.Data.Complex.Basic
  (r s : ℝ) : ↑(r - s) = ↑r - ↑s
• Complex.re_mul_ofReal 📋 Mathlib.Data.Complex.Basic
  (z : ℂ) (r : ℝ) : (z * ↑r).re = z.re * r
• Complex.re_ofReal_mul 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re
• Complex.div_ofReal_im 📋 Mathlib.Data.Complex.Basic
  (z : ℂ) (x : ℝ) : (z / ↑x).im = z.im / x
• Complex.div_ofReal_re 📋 Mathlib.Data.Complex.Basic
  (z : ℂ) (x : ℝ) : (z / ↑x).re = z.re / x
• Complex.ofRealHom_eq_coe 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : Complex.ofRealHom r = ↑r
• Complex.ofReal_div 📋 Mathlib.Data.Complex.Basic
  (r s : ℝ) : ↑(r / s) = ↑r / ↑s
• Complex.ofReal_zpow 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) (n : ℤ) : ↑(r ^ n) = ↑r ^ n
• Complex.ofReal_nsmul 📋 Mathlib.Data.Complex.Basic
  (n : ℕ) (r : ℝ) : ↑(n • r) = n • ↑r
• Complex.ofReal_pow 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) (n : ℕ) : ↑(r ^ n) = ↑r ^ n
• Complex.ofReal_mul' 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) (z : ℂ) : ↑r * z = { re := r * z.re, im := r * z.im }
• Complex.ofReal_comp_neg 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (f : α → ℝ) : Complex.ofReal ∘ (-f) = -Complex.ofReal ∘ f
• Complex.ofReal_zsmul 📋 Mathlib.Data.Complex.Basic
  (n : ℤ) (r : ℝ) : ↑(n • r) = n • ↑r
• Complex.conj_ofReal 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : (starRingEnd ℂ) ↑r = ↑r
• Complex.div_ofReal 📋 Mathlib.Data.Complex.Basic
  (z : ℂ) (x : ℝ) : z / ↑x = { re := z.re / x, im := z.im / x }
• Complex.normSq_ofReal 📋 Mathlib.Data.Complex.Basic
  (r : ℝ) : Complex.normSq ↑r = r * r
• Complex.ofReal_comp_add 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (f g : α → ℝ) : Complex.ofReal ∘ (f + g) = Complex.ofReal ∘ f + Complex.ofReal ∘ g
• Complex.ofReal_comp_mul 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (f g : α → ℝ) : Complex.ofReal ∘ (f * g) = Complex.ofReal ∘ f * Complex.ofReal ∘ g
• Complex.ofReal_comp_sub 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (f g : α → ℝ) : Complex.ofReal ∘ (f - g) = Complex.ofReal ∘ f - Complex.ofReal ∘ g
• Complex.ofReal_comp_nsmul 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (n : ℕ) (f : α → ℝ) : Complex.ofReal ∘ (n • f) = n • Complex.ofReal ∘ f
• Complex.ofReal_comp_pow 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (f : α → ℝ) (n : ℕ) : Complex.ofReal ∘ (f ^ n) = Complex.ofReal ∘ f ^ n
• Complex.ofReal_qsmul 📋 Mathlib.Data.Complex.Basic
  (q : ℚ) (r : ℝ) : ↑(q • r) = q • ↑r
• Complex.ofReal_comp_zsmul 📋 Mathlib.Data.Complex.Basic
  {α : Type u_1} (n : ℤ) (f : α → ℝ) : Complex.ofReal ∘ (n • f) = n • Complex.ofReal ∘ f
• Complex.ofReal_nnqsmul 📋 Mathlib.Data.Complex.Basic
  (q : ℚ≥0) (r : ℝ) : ↑(q • r) = q • ↑r
• Complex.normSq_ofReal_add_I_mul_sqrt_one_sub 📋 Mathlib.Analysis.Complex.Norm
  {x : ℝ} (hx : ‖x‖ ≤ 1) : Complex.normSq (↑x + Complex.I * ↑√(1 - x ^ 2)) = 1
• Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub 📋 Mathlib.Analysis.Complex.Norm
  {x : ℝ} (hx : ‖x‖ ≤ 1) : Complex.normSq (↑x - Complex.I * ↑√(1 - x ^ 2)) = 1
• Complex.monotone_ofReal 📋 Mathlib.Analysis.Complex.Order
  : Monotone Complex.ofReal
• Complex.eq_re_of_ofReal_le 📋 Mathlib.Analysis.Complex.Order
  {r : ℝ} {z : ℂ} (hz : ↑r ≤ z) : z = ↑z.re
• Complex.ofReal_prod 📋 Mathlib.Data.Complex.BigOperators
  {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
• Complex.ofReal_sum 📋 Mathlib.Data.Complex.BigOperators
  {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
• Complex.ofReal_balance 📋 Mathlib.Data.Complex.BigOperators
  {α : Type u_1} [Fintype α] (f : α → ℝ) (a : α) : ↑(Fintype.balance f a) = Fintype.balance (Complex.ofReal ∘ f) a
• Complex.ofReal_comp_balance 📋 Mathlib.Data.Complex.BigOperators
  {ι : Type u_2} [Fintype ι] (f : ι → ℝ) : Complex.ofReal ∘ Fintype.balance f = Fintype.balance (Complex.ofReal ∘ f)
• Complex.ofReal_expect 📋 Mathlib.Data.Complex.BigOperators
  {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(s.expect fun i => f i) = s.expect fun i => ↑(f i)
• Complex.instAlgebraOfReal 📋 Mathlib.LinearAlgebra.Complex.Module
  {R : Type u_1} [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ
• Complex.ofRealAm 📋 Mathlib.LinearAlgebra.Complex.Module
  : ℝ →ₐ[ℝ] ℂ
• Complex.instIsCentralScalarOfReal 📋 Mathlib.LinearAlgebra.Complex.Module
  {R : Type u_1} [SMul R ℝ] [SMul Rᵐᵒᵖ ℝ] [IsCentralScalar R ℝ] : IsCentralScalar R ℂ
• Complex.instSMulCommClassOfReal 📋 Mathlib.LinearAlgebra.Complex.Module
  {R : Type u_1} {S : Type u_2} [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] : SMulCommClass R S ℂ
• Complex.instDistribMulActionOfReal 📋 Mathlib.LinearAlgebra.Complex.Module
  {R : Type u_1} [Semiring R] [DistribMulAction R ℝ] : DistribMulAction R ℂ
• Complex.instIsScalarTowerOfReal 📋 Mathlib.LinearAlgebra.Complex.Module
  {R : Type u_1} {S : Type u_2} [SMul R S] [SMul R ℝ] [SMul S ℝ] [IsScalarTower R S ℝ] : IsScalarTower R S ℂ
• Complex.ofRealAm_coe 📋 Mathlib.LinearAlgebra.Complex.Module
  : ⇑Complex.ofRealAm = Complex.ofReal
• Complex.isometry_ofReal 📋 Mathlib.Analysis.Complex.Basic
  : Isometry Complex.ofReal
• Complex.isUniformEmbedding_ofReal 📋 Mathlib.Analysis.Complex.Basic
  : IsUniformEmbedding Complex.ofReal
• Complex.ofReal_mem_slitPlane 📋 Mathlib.Analysis.Complex.Basic
  {x : ℝ} : ↑x ∈ Complex.slitPlane ↔ 0 < x
• Complex.continuous_ofReal 📋 Mathlib.Analysis.Complex.Basic
  : Continuous Complex.ofReal
• Complex.instNormedAlgebraOfReal 📋 Mathlib.Analysis.Complex.Basic
  {R : Type u_1} [NormedField R] [NormedAlgebra R ℝ] : NormedAlgebra R ℂ
• Complex.neg_ofReal_mem_slitPlane 📋 Mathlib.Analysis.Complex.Basic
  {x : ℝ} : -↑x ∈ Complex.slitPlane ↔ x < 0
• Complex.ofReal_eq_re_of_isSelfAdjoint 📋 Mathlib.Analysis.Complex.Basic
  {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) : y = x.re ↔ ↑y = x
• Complex.re_eq_ofReal_of_isSelfAdjoint 📋 Mathlib.Analysis.Complex.Basic
  {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) : x.re = y ↔ x = ↑y
• Complex.ringHom_eq_ofReal_of_continuous 📋 Mathlib.Analysis.Complex.Basic
  {f : ℝ →+* ℂ} (h : Continuous ⇑f) : f = Complex.ofRealHom
• Complex.summable_ofReal 📋 Mathlib.Analysis.Complex.Basic
  {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} : Summable (fun x => ↑(f x)) L ↔ Summable f L
• Complex.hasSum_ofReal 📋 Mathlib.Analysis.Complex.Basic
  {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {x : ℝ} : HasSum (fun x => ↑(f x)) (↑x) L ↔ HasSum f x L
• Complex.ofReal_tsum 📋 Mathlib.Analysis.Complex.Basic
  {α : Type u_1} {L : SummationFilter α} (f : α → ℝ) : ↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
• Complex.ofRealLI 📋 Mathlib.Analysis.Complex.Basic
  : ℝ →ₗᵢ[ℝ] ℂ
• Complex.ofRealCLM 📋 Mathlib.Analysis.Complex.Basic
  : ℝ →L[ℝ] ℂ
• Complex.ofRealLI_apply 📋 Mathlib.Analysis.Complex.Basic
  (x : ℝ) : Complex.ofRealLI x = ↑x
• Complex.ofRealCLM_coe 📋 Mathlib.Analysis.Complex.Basic
  : ↑Complex.ofRealCLM = Complex.ofRealAm.toLinearMap
• Complex.ofRealCLM_apply 📋 Mathlib.Analysis.Complex.Basic
  (x : ℝ) : Complex.ofRealCLM x = ↑x
• Complex.isTheta_ofReal 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} (f : α → ℝ) (l : Filter α) : (fun x => ↑(f x)) =Θ[l] f
• Complex.isBigO_ofReal_left 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → ℝ} {g : α → E} : (fun x => ↑(f x)) =O[l] g ↔ f =O[l] g
• Complex.isBigO_ofReal_right 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → E} {g : α → ℝ} : (f =O[l] fun x => ↑(g x)) ↔ f =O[l] g
• Complex.isLittleO_ofReal_left 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → ℝ} {g : α → E} : (fun x => ↑(f x)) =o[l] g ↔ f =o[l] g
• Complex.isLittleO_ofReal_right 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → E} {g : α → ℝ} : (f =o[l] fun x => ↑(g x)) ↔ f =o[l] g
• Complex.isTheta_ofReal_left 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → ℝ} {g : α → E} : (fun x => ↑(f x)) =Θ[l] g ↔ f =Θ[l] g
• Complex.isTheta_ofReal_right 📋 Mathlib.Analysis.Complex.Asymptotics
  {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {f : α → E} {g : α → ℝ} : (f =Θ[l] fun x => ↑(g x)) ↔ f =Θ[l] g
• Complex.isBigO_comp_ofReal_nhds 📋 Mathlib.Analysis.Complex.Asymptotics
  {f g : ℂ → ℂ} {x : ℝ} (h : f =O[nhds ↑x] g) : (fun y => f ↑y) =O[nhds x] fun y => g ↑y
• Complex.isBigO_comp_ofReal_nhds_ne 📋 Mathlib.Analysis.Complex.Asymptotics
  {f g : ℂ → ℂ} {x : ℝ} (h : f =O[nhdsWithin ↑x {↑x}ᶜ] g) : (fun y => f ↑y) =O[nhdsWithin x {x}ᶜ] fun y => g ↑y
• Complex.exp_ofReal_re 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) : (Complex.exp ↑x).re = Real.exp x
• Complex.ofReal_exp 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) : ↑(Real.exp x) = Complex.exp ↑x
• Complex.norm_exp_ofReal 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) : ‖Complex.exp ↑x‖ = Real.exp x
• Complex.ofReal_exp_ofReal_re 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) : ↑(Complex.exp ↑x).re = Complex.exp ↑x
• Complex.exp_ofReal_im 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) : (Complex.exp ↑x).im = 0
• Complex.cos_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.cos ↑x).re = Real.cos x
• Complex.cosh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.cosh ↑x).re = Real.cosh x
• Complex.ofReal_cos 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.cos x) = Complex.cos ↑x
• Complex.ofReal_cosh 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.cosh x) = Complex.cosh ↑x
• Complex.ofReal_cot 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑x.cot = (↑x).cot
• Complex.ofReal_sin 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.sin x) = Complex.sin ↑x
• Complex.ofReal_sinh 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.sinh x) = Complex.sinh ↑x
• Complex.ofReal_tan 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.tan x) = Complex.tan ↑x
• Complex.ofReal_tanh 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Real.tanh x) = Complex.tanh ↑x
• Complex.sin_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.sin ↑x).re = Real.sin x
• Complex.sinh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.sinh ↑x).re = Real.sinh x
• Complex.tan_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.tan ↑x).re = Real.tan x
• Complex.tanh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.tanh ↑x).re = Real.tanh x
• Complex.ofReal_cos_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.cos ↑x).re = Complex.cos ↑x
• Complex.ofReal_cosh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.cosh ↑x).re = Complex.cosh ↑x
• Complex.ofReal_cot_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(↑x).cot.re = (↑x).cot
• Complex.ofReal_sin_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.sin ↑x).re = Complex.sin ↑x
• Complex.ofReal_sinh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.sinh ↑x).re = Complex.sinh ↑x
• Complex.ofReal_tan_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.tan ↑x).re = Complex.tan ↑x
• Complex.ofReal_tanh_ofReal_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ↑(Complex.tanh ↑x).re = Complex.tanh ↑x
• Complex.cos_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.cos ↑x).im = 0
• Complex.cosh_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.cosh ↑x).im = 0
• Complex.sin_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.sin ↑x).im = 0
• Complex.sinh_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.sinh ↑x).im = 0
• Complex.tan_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.tan ↑x).im = 0
• Complex.tanh_ofReal_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.tanh ↑x).im = 0
• Complex.exp_ofReal_mul_I_im 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.exp (↑x * Complex.I)).im = Real.sin x
• Complex.exp_ofReal_mul_I_re 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : (Complex.exp (↑x * Complex.I)).re = Real.cos x
• Complex.norm_exp_I_mul_ofReal 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ = 1
• Complex.norm_exp_ofReal_mul_I 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (↑x * Complex.I)‖ = 1
• Complex.nnnorm_exp_I_mul_ofReal 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖₊ = 1
• Complex.nnnorm_exp_ofReal_mul_I 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (↑x * Complex.I)‖₊ = 1
• Complex.enorm_exp_I_mul_ofReal 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ₑ = 1
• Complex.enorm_exp_ofReal_mul_I 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (↑x * Complex.I)‖ₑ = 1
• Complex.norm_exp_I_mul_ofReal_sub_one 📋 Mathlib.Analysis.Complex.Trigonometric
  (x : ℝ) : ‖Complex.exp (Complex.I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖
• Complex.arg_ofReal_of_neg 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {x : ℝ} (hx : x < 0) : (↑x).arg = Real.pi
• Complex.arg_ofReal_of_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arg
  {x : ℝ} (hx : 0 ≤ x) : (↑x).arg = 0
• Complex.log_ofReal_re 📋 Mathlib.Analysis.SpecialFunctions.Complex.Log
  (x : ℝ) : (Complex.log ↑x).re = Real.log x
• Complex.ofReal_log 📋 Mathlib.Analysis.SpecialFunctions.Complex.Log
  {x : ℝ} (hx : 0 ≤ x) : ↑(Real.log x) = Complex.log ↑x
• Complex.log_mul_ofReal 📋 Mathlib.Analysis.SpecialFunctions.Complex.Log
  (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) : Complex.log (x * ↑r) = ↑(Real.log r) + Complex.log x
• Complex.log_ofReal_mul 📋 Mathlib.Analysis.SpecialFunctions.Complex.Log
  {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) : Complex.log (↑r * x) = ↑(Real.log r) + Complex.log x
• Complex.mul_cpow_ofReal_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Pow.Complex
  {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) : (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
• Complex.norm_ofReal_cpow_eventually_eq_atTop 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  (c : ℂ) : (fun t => ‖↑t ^ c‖) =ᶠ[Filter.atTop] fun t => t ^ c.re
• Complex.ofReal_cpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : ↑(x ^ y) = ↑x ^ ↑y
• Complex.inv_natCast_cpow_ofReal_pos 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {n : ℕ} (hn : n ≠ 0) (x : ℝ) : 0 < (↑n ^ ↑x)⁻¹
• Complex.cpow_ofReal_im 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  (x : ℂ) (y : ℝ) : (x ^ ↑y).im = ‖x‖ ^ y * Real.sin (x.arg * y)
• Complex.cpow_ofReal_re 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  (x : ℂ) (y : ℝ) : (x ^ ↑y).re = ‖x‖ ^ y * Real.cos (x.arg * y)
• Complex.cpow_mul_ofReal_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (z : ℂ) : ↑x ^ (↑y * z) = ↑(x ^ y) ^ z
• Complex.ofReal_cpow_of_nonpos 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : x ≤ 0) (y : ℂ) : ↑x ^ y = (-↑x) ^ y * Complex.exp (↑Real.pi * Complex.I * y)
• Complex.cpow_ofReal 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  (x : ℂ) (y : ℝ) : x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * Complex.I)
• Complex.continuous_ofReal_cpow_const 📋 Mathlib.Analysis.SpecialFunctions.Pow.Continuity
  {y : ℂ} (hs : 0 < y.re) : Continuous fun x => ↑x ^ y
• Complex.continuousAt_ofReal_cpow_const 📋 Mathlib.Analysis.SpecialFunctions.Pow.Continuity
  (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) : ContinuousAt (fun a => ↑a ^ y) x
• Complex.continuousAt_ofReal_cpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Continuity
  (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) : ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
• Complex.measurable_ofReal 📋 Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
  : Measurable Complex.ofReal
• Complex.starConvex_ofReal_slitPlane 📋 Mathlib.Analysis.Complex.Convex
  {x : ℝ} (hx : 0 < x) : StarConvex ℝ (↑x) Complex.slitPlane
• Complex.deriv_ofReal_cpow_const 📋 Mathlib.Analysis.SpecialFunctions.Pow.Deriv
  {c : ℂ} {x : ℝ} (hx : x ≠ 0) (hc : c ≠ 0) : deriv (fun x => ↑x ^ c) x = c * ↑x ^ (c - 1)
• Complex.ofRealCLM_norm 📋 Mathlib.Analysis.Complex.OperatorNorm
  : ‖Complex.ofRealCLM‖ = 1
• Complex.ofRealCLM_nnnorm 📋 Mathlib.Analysis.Complex.OperatorNorm
  : ‖Complex.ofRealCLM‖₊ = 1
• Complex.ofRealCLM_enorm 📋 Mathlib.Analysis.Complex.OperatorNorm
  : ‖Complex.ofRealCLM‖ₑ = 1
• Complex.Gamma_ofReal 📋 Mathlib.Analysis.SpecialFunctions.Gamma.Basic
  (s : ℝ) : Complex.Gamma ↑s = ↑(Real.Gamma s)
• Complex.GammaIntegral_ofReal 📋 Mathlib.Analysis.SpecialFunctions.Gamma.Basic
  (s : ℝ) : (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1))
• Complex.ofRealLI.eq_1 📋 Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
  : Complex.ofRealLI = { toLinearMap := Complex.ofRealAm.toLinearMap, norm_map' := Complex.norm_real }
• Complex.ofReal_arctan 📋 Mathlib.Analysis.SpecialFunctions.Complex.Arctan
  (x : ℝ) : ↑(Real.arctan x) = (↑x).arctan

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 187ba29 serving mathlib revision 00a7199