Mathlib Map

Theorems · Definition · ring theory

IsSelfAdjoint

{R : Type u_1} → [Star R] → R → Prop

An element is self-adjoint if it is equal to its star.

Defined in
Mathlib.Algebra.Star.SelfAdjoint
Cited by
545 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 4 definitions · uses no axioms
Assumes
Star
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

selfAdjoint · cited by 135selfAdjointCFC.sqrt · cited by 82CFC.sqrtIsSelfAdjoint.star_eq · cited by 58IsSelfAdjoint.star_eqCFC.abs · cited by 43CFC.absIsSelfAdjoint.of_nonneg · cited by 43IsSelfAdjoint.of_nonnegNumberField.ComplexEmbedding.IsReal · cited by 38ComplexEmbedding.IsRealLE.le.isSelfAdjoint · cited by 20le.isSelfAdjointIsStarProjection.isSelfAdjoint · cited by 18IsStarProjection.isSelfAd…CFC.log · cited by 17CFC.logCFC.conjSqrt · cited by 13CFC.conjSqrtIsSelfAdjoint.spectrumRestricts · cited by 13IsSelfAdjoint.spectrumRes…IsSelfAdjoint.sub · cited by 13IsSelfAdjoint.subIsSelfAdjoint.star_mul_self · cited by 12IsSelfAdjoint.star_mul_se…CFC.sqrt_mul_sqrt_self · cited by 11CFC.sqrt_mul_sqrt_selfCFC.sqrt_nonneg · cited by 11CFC.sqrt_nonnegStar.star · cited by 1082Star.starStar · cited by 496StarIsSelfAdjointCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Star.starproof · cited by 1,082
  • Starstatement and proof · cited by 496

Cited by559

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 559.