Mathlib Map

Theorems · Definition · ring theory

NonUnitalStarSubsemiring.center

(R : Type u_1) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : StarRing R] → NonUnitalStarSubsemiring R

The center of a non-unital non-associative semiring R is the set of elements that commute and associate with everything in R, here realized as a non-unital star subsemiring.

Defined in
Mathlib.Algebra.Star.NonUnitalSubsemiring
Cited by
3 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NonUnitalNonAssocSemiringStarRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CentroidHom.starCenterIsoCentroid · cited by 2CentroidHom.starCenterIso…CentroidHom.starCenterToCentroid · cited by 2CentroidHom.starCenterToC…CentroidHom.starCenterIsoCentroid_apply · cited by 0CentroidHom.starCenterIso…CentroidHom.starCenterToCentroidCenter · cited by 0CentroidHom.starCenterToC…CentroidHom.starCenterToCentroid_apply · cited by 0CentroidHom.starCenterToC…CentroidHom.star_centerToCentroidCenter · cited by 0CentroidHom.star_centerTo…StarRing · cited by 1686StarRingNonUnitalNonAssocSemiring · cited by 1081NonUnitalNonAssocSemiringNonUnitalSubsemiring · cited by 201NonUnitalSubsemiringNonUnitalSubsemiring.center · cited by 22NonUnitalSubsemiring.cent…NonUnitalStarSubsemiring · cited by 11NonUnitalStarSubsemiringNonUnitalStarSubsemiring.cent…CITED BYCITES

Cites5

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

Cited by6

Results whose statement or proof uses this declaration.