Theorems · Definition · commutative algebra
Subsemiring.center
(R : Type u) → [inst : NonAssocSemiring R] → Subsemiring R
The center of a non-associative semiring R is the set of elements that commute and associate
with everything in R
- Defined in
- Mathlib.Algebra.Ring.Subsemiring.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonAssocSemiringstatement and proof · cited by 805
- Subsemiringstatement · cited by 456
- NonUnitalSubsemiringproof · cited by 201
- AddSubmonoid.toAddSubsemigroupproof · cited by 198
- AddSubsemigroup.carrierproof · cited by 198
- NonUnitalSubsemiring.toAddSubmonoidproof · cited by 56
- NonUnitalSubsemiring.centerproof · cited by 22
Cited by29
Results whose statement or proof uses this declaration.
- Subring.centerproof · cited by 28
- Subalgebra.centerproof · cited by 24
- Subsemiring.centerCongrstatement · cited by 2
- CentroidHom.centerToCentroidCenterstatement · cited by 2
- Subsemiring.centerToMulOppositestatement · cited by 2
- StarSubsemiring.centerproof · cited by 2
- CentroidHom.centerToCentroidproof · cited by 2
- Subalgebra.center_toSubsemiringstatement · cited by 0
- Subsemiring.centerCongr_apply_coestatement · cited by 0
- CentroidHom.centerIsoCentroidstatement · cited by 0
- CentroidHom.centerStarEmbeddingstatement and proof · cited by 0
- Subsemiring.centerCongr_symm_apply_coestatement · cited by 0