Theorems · Definition · ring theory
NonUnitalSubsemiring.center
(R : Type u) → [inst : NonUnitalNonAssocSemiring R] → NonUnitalSubsemiring R
The center of a semiring R is the set of elements that commute and associate with everything
in R
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonUnitalNonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Subsemigroupproof · cited by 323
- NonUnitalSubsemiringstatement · cited by 201
- Subsemigroup.carrierproof · cited by 160
- Subsemigroup.centerproof · cited by 38
Cited by31
Results whose statement or proof uses this declaration.
- Subsemiring.centerproof · cited by 18
- NonUnitalSubring.centerproof · cited by 13
- NonUnitalSubalgebra.centerproof · cited by 8
- NonUnitalStarSubsemiring.centerproof · cited by 3
- CentroidHom.centerToCentroidstatement · cited by 2
- CentroidHom.centerToCentroidCenterstatement and proof · cited by 2
- NonUnitalSubsemiring.centerCongrstatement · cited by 2
- NonUnitalSubsemiring.centerToMulOppositestatement · cited by 2
- NonUnitalNonAssocSemiring.mem_center_iffstatement and proof · cited by 1
- CentroidHom.centerIsoCentroidproof · cited by 0
- CentroidHom.centerToCentroidCenter_applystatement and proof · cited by 0
- CentroidHom.centerToCentroid_applystatement and proof · cited by 0