Mathlib Map

Theorems · Theorem · ring theory

TrivialStar.star_trivial

∀ {R : Type u} {inst : Star R} [self : TrivialStar R] (r : R), star r = r

Condition that star is trivial

Defined in
Mathlib.Algebra.Star.Basic
Cited by
26 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
TrivialStar
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

conj_trivial · cited by 27conj_trivialIsSelfAdjoint.all · cited by 5IsSelfAdjoint.allSimpleGraph.posSemidef_lapMatrix · cited by 2SimpleGraph.posSemidef_la…CStarModule.inner_smul_left_real · cited by 2CStarModule.inner_smul_le…OrthonormalBasis.det_to_matrix_orthonormalBasis_real · cited by 2OrthonormalBasis.det_to_m…CFC.abs_smul_nonneg · cited by 2CFC.abs_smul_nonnegMatrix.conjTranspose_eq_transpose_of_trivial · cited by 2Matrix.conjTranspose_eq_t…SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable · cited by 2SimpleGraph.lapMatrix_mul…Matrix.PosDef.of_toQuadraticForm' · cited by 1PosDef.of_toQuadraticForm'Unitary.mem_iff_eq_one_or_eq_neg_one · cited by 1Unitary.mem_iff_eq_one_or…Matrix.PosDef.toQuadraticForm' · cited by 1PosDef.toQuadraticForm'CStarModule.inner_smul_right_real · cited by 1CStarModule.inner_smul_ri…spectrum_star_mul_self_nonneg · cited by 1spectrum_star_mul_self_no…LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix · cited by 1BilinForm.posDef_toQuadra…InnerProductGeometry.norm_ofLp_crossProduct · cited by 1InnerProductGeometry.norm…Star.star · cited by 1082Star.starStar · cited by 496StarTrivialStar · cited by 66TrivialStarTrivialStar.star_trivialCITED BYCITES

Cites3

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

  • Star.starstatement · cited by 1,082
  • Starstatement and proof · cited by 496
  • TrivialStarstatement and proof · cited by 66

Cited by26

Results whose statement or proof uses this declaration.