Mathlib Map

Theorems · Inductive type · ring theory

StarHomClass

(F : Type u_1) → (R : outParam (Type u_2)) → (S : outParam (Type u_3)) → [Star R] → [Star S] → [FunLike F R S] → Prop

StarHomClass F R S states that F is a type of star-preserving maps from R to S.

Defined in
Mathlib.Algebra.Star.Basic
Cited by
76 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
StarStarFunLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NonUnitalStarAlgHom.range · cited by 24NonUnitalStarAlgHom.rangeNonUnitalStarAlgHomClass.toNonUnitalStarAlgHom · cited by 23NonUnitalStarAlgHomClass.…NonUnitalStarSubalgebra.map · cited by 23NonUnitalStarSubalgebra.m…StarHomClass.map_star · cited by 20StarHomClass.map_starIsSelfAdjoint.map · cited by 7IsSelfAdjoint.mapStarAlgHomClass.toStarAlgHom · cited by 7StarAlgHomClass.toStarAlg…DirectLimit.NonUnitalStarRing.of · cited by 6NonUnitalStarRing.ofNonUnitalStarAlgHom.codRestrict · cited by 5NonUnitalStarAlgHom.codRe…NonUnitalStarSubalgebra.comap · cited by 5NonUnitalStarSubalgebra.c…StarAlgHom.equalizer · cited by 4StarAlgHom.equalizerNonUnitalStarAlgHom.coe_range · cited by 3NonUnitalStarAlgHom.coe_r…NonUnitalStarAlgHom.map_adjoin · cited by 3NonUnitalStarAlgHom.map_a…DirectLimit.NonUnitalStarRing.lift · cited by 3NonUnitalStarRing.liftStarAlgEquiv.ofBijective · cited by 2StarAlgEquiv.ofBijectiveStarAlgEquiv.ofLeftInverse' · cited by 2StarAlgEquiv.ofLeftInvers…FunLike · cited by 2560FunLikeStar · cited by 496StarStarHomClassCITED BYCITES

Cites2

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

  • FunLikestatement · cited by 2,560
  • Starstatement · cited by 496

Cited by97

Results whose statement or proof uses this declaration.