Theorems · Definition · functional analysis
Unitary.argSelfAdjoint
{A : Type u_1} → [inst : CStarAlgebra A] → ↥(unitary A) → ↥(selfAdjoint A)The selfadjoint element obtained by taking the argument (using the principal branch and the
continuous functional calculus) of a unitary whose spectrum does not contain -1. This returns
0 if the principal branch of the logarithm is not continuous on the spectrum of the unitary
element.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 313 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CStarAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexproof · cited by 5,565
- AddSubgroupstatement · cited by 3,232
- Submonoidstatement · cited by 3,086
- Complex.ofRealproof · cited by 1,654
- cfcproof · cited by 228
- Complex.argproof · cited by 220
- unitarystatement and proof · cited by 207
- selfAdjointstatement · cited by 135
- CStarAlgebrastatement and proof · cited by 123
Cited by15
Results whose statement or proof uses this declaration.
- Unitary.argSelfAdjoint_coestatement and proof · cited by 4
- Unitary.openPartialHomeomorphproof · cited by 4
- Unitary.pathproof · cited by 4
- Unitary.norm_argSelfAdjoint_le_pistatement · cited by 3
- Unitary.two_mul_one_sub_cos_norm_argSelfAdjointstatement and proof · cited by 2
- expUnitary_argSelfAdjointstatement and proof · cited by 2
- Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_lestatement and proof · cited by 1
- Unitary.expUnitary_eq_mul_invstatement · cited by 1
- Unitary.path_applystatement · cited by 1
- Unitary.mem_pathComponentOne_iffproof · cited by 0
- argSelfAdjoint_expUnitarystatement and proof · cited by 0
- Unitary.norm_argSelfAdjointstatement and proof · cited by 0