Theorems · Theorem · functional analysis

CFC.rpow_eq_rpow_pi

∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → Ring (C i)]
  [inst_2 : (i : ι) → StarRing (C i)] [inst_3 : (i : ι) → TopologicalSpace (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Algebra ℝ (C i)] [inst_7 : ∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_8 : ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsSemitopologicalRing (C i)]
  [∀ (i : ι), T2Space (C i)] [inst_11 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_12 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : ℝ},
  (∀ (i : ι), IsUnit (c i)) → autoParam (∀ (i : ι), 0 ≤ c i) CFC.rpow_eq_rpow_pi._auto_1 → CFC.rpow c x = c ^ x

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Cited by

0 results in Mathlib

Foundations

Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderRingStarRingTopologicalSpaceStarOrderedRingStarOrderedRingAlgebraContinuousFunctionalCalculusContinuousFunctionalCalculusIsSemitopologicalRingT2SpaceNonnegSpectrumClassNonnegSpectrumClass