Theorems · Theorem · functional analysis

CFC.nnrpow_eq_nnrpow_pi

∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → NonUnitalRing (C i)]
  [inst_2 : (i : ι) → TopologicalSpace (C i)] [inst_3 : (i : ι) → StarRing (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Module ℝ (C i)] [inst_7 : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)]
  [inst_8 : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)]
  [inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint]
  [∀ (i : ι), IsSemitopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_14 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : NNReal},
  autoParam (∀ (i : ι), 0 ≤ c i) CFC.nnrpow_eq_nnrpow_pi._auto_1 → CFC.nnrpow 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

PartialOrderNonUnitalRingTopologicalSpaceStarRingStarOrderedRingStarOrderedRingModuleSMulCommClassIsScalarTowerNonUnitalContinuousFunctionalCalculusNonUnitalContinuousFunctionalCalculusIsSemitopologicalRingT2SpaceNonnegSpectrumClassNonnegSpectrumClass