Theorems · Theorem · functional analysis
CStarRing.norm_of_mem_unitary
∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] [Nontrivial E] {U : E},
U ∈ unitary E → ‖U‖ = 1- Defined in
- Mathlib.Analysis.CStarAlgebra.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- Submonoidstatement · cited by 3,086
- Nontrivialstatement and proof · cited by 2,416
- StarRingstatement and proof · cited by 1,686
- NormedRingstatement and proof · cited by 924
- unitarystatement and proof · cited by 207
- CStarRingstatement and proof · cited by 61
- CStarRing.norm_coe_unitaryproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrictproof · cited by 8
- LinearIsometry.normDet_eq_oneproof · cited by 4
- MeasureTheory.contDiff_charFunproof · cited by 2
- circleAverage_log_norm_sub_const₀proof · cited by 1
- MeasureTheory.iteratedFDeriv_charFunproof · cited by 1
- MeasureTheory.contDiff_charFun'proof · cited by 0