Theorems · Inductive type
Star
Type u → Type u
Notation typeclass (with no default notation!) for an algebraic structure with a star operation.
- Defined in
- Mathlib.Algebra.Notation.Defs
- Cited by
- 496 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by728
Results whose statement or proof uses this declaration.
- Star.starstatement and proof · cited by 1,082
- StarModulestatement · cited by 570
- IsSelfAdjointstatement and proof · cited by 545
- ContinuousStarstatement · cited by 543
- StarAlgHomstatement · cited by 215
- NonUnitalStarAlgHomstatement · cited by 208
- Matrix.conjTransposestatement and proof · cited by 202
- NonUnitalStarSubalgebrastatement · cited by 196
- StarAlgEquivstatement · cited by 132
- Matrix.IsHermitianstatement and proof · cited by 126
- IsStarNormalstatement · cited by 117
- StarHomClassstatement · cited by 76
Showing the 200 most cited of 728.