Theorems · Theorem · functional analysis

CFC.complex_exp_eq_normedSpace_exp

∀ {A : Type u_1} {p : A → Prop} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℂ A]
  [inst_3 : ContinuousFunctionalCalculus ℂ A p] {a : A},
  autoParam (p a) CFC.complex_exp_eq_normedSpace_exp._auto_1 → cfc Complex.exp a = NormedSpace.exp a

Defined in: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedRing StarRing NormedAlgebra ContinuousFunctionalCalculus

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Complexstatement and proof · cited by 5,565
StarRingstatement and proof · cited by 1,686
NormedAlgebrastatement and proof · cited by 1,165
NormedRingstatement and proof · cited by 924
Complex.expstatement · cited by 612
ContinuousFunctionalCalculusstatement and proof · cited by 331
cfcstatement · cited by 228
NormedSpace.expstatement · cited by 157
Complex.exp_eq_exp_ℂproof · cited by 8
CFC.exp_eq_normedSpace_expproof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.