Theorems · Definition · commutative algebra
Subring.center
(R : Type u) → [inst : NonAssocRing R] → Subring R
The center of a ring R is the set of elements that commute with everything in R
- Defined in
- Mathlib.Algebra.Ring.Subring.Basic
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocRing
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.
- Subringstatement · cited by 602
- NonAssocRingstatement and proof · cited by 483
- Subsemiringproof · cited by 456
- Set.centerproof · cited by 49
- Subsemiring.centerproof · cited by 18
Cited by30
Results whose statement or proof uses this declaration.
- Subring.mem_center_iffstatement · cited by 3
- Subring.centerCongrstatement · cited by 2
- Subring.centerToMulOppositestatement · cited by 2
- JacobsonNoether.exists_pow_mem_center_of_inseparablestatement and proof · cited by 2
- LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependentstatement · cited by 1
- LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basisstatement and proof · cited by 1
- Subring.center_eq_topstatement and proof · cited by 1
- JacobsonNoether.exist_pow_eq_zero_of_lestatement and proof · cited by 1
- JacobsonNoether.exists_pow_mem_center_of_inseparable'statement and proof · cited by 1
- JacobsonNoether.exists_separable_and_not_isCentralstatement and proof · cited by 1
- Subalgebra.center_toSubringstatement · cited by 1
- IsSimpleRing.isField_centerstatement and proof · cited by 1