Theorems · Theorem · functional analysis
StarSubalgebra.coe_isUnit
∀ {A : Type u_1} [inst : CStarAlgebra A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : ↥S}, IsUnit ↑a ↔ IsUnit aFor a unital C⋆-subalgebra S of A and x : S, if ↑x : A is invertible in A, then
x is invertible in S.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Spectrum
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CStarAlgebraIsClosed
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- SetLike.coestatement and proof · cited by 8,199
- Complexstatement and proof · cited by 5,565
- Units.valproof · cited by 1,966
- mul_assocproof · cited by 1,667
- IsClosedstatement and proof · cited by 1,639
- IsUnitstatement and proof · cited by 1,602
- Star.starproof · cited by 1,082
- IsSelfAdjointproof · cited by 545
- spectrumproof · cited by 510
- IsUnit.unitproof · cited by 252
- StarSubalgebrastatement and proof · cited by 194
Cited by1
Results whose statement or proof uses this declaration.
- StarSubalgebra.mem_spectrum_iffproof · cited by 1