Theorems · Theorem · functional analysis

CFC.negPart_def

∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a⁻ = cfcₙ (fun x => x⁻) a

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

NonUnitalRingModuleSMulCommClassIsScalarTowerStarRingTopologicalSpaceNonUnitalContinuousFunctionalCalculus