Mathlib Map

Theorems · Definition

Star.star

{R : Type u} → [self : Star R] → R → R

A star operation (e.g. complex conjugate).

Defined in
Mathlib.Algebra.Notation.Defs
Cited by
1,082 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Assumes
Star
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

starRingEnd · cited by 671starRingEndIsSelfAdjoint · cited by 545IsSelfAdjointunitary · cited by 207unitaryMatrix.conjTranspose · cited by 202Matrix.conjTransposestar_star · cited by 135star_starMatrix.PosSemidef · cited by 76Matrix.PosSemidefStarMul.star_mul · cited by 72StarMul.star_mulMatrix.PosDef · cited by 68Matrix.PosDefIsSelfAdjoint.star_eq · cited by 58IsSelfAdjoint.star_eqstar_zero · cited by 58star_zeroNonUnitalStarAlgebra.adjoin · cited by 43NonUnitalStarAlgebra.adjo…CFC.abs · cited by 43CFC.absStarAlgebra.adjoin · cited by 42StarAlgebra.adjoinNumberField.ComplexEmbedding.conjugate · cited by 40ComplexEmbedding.conjugateNumberField.maximalRealSubfield · cited by 38NumberField.maximalRealSu…Star · cited by 496StarStar.starCITED BYCITES

Cites1

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

  • Starstatement and proof · cited by 496

Cited by1,232

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 1,232.