Theorems · Theorem · nonassociative algebras
CentroidHom.centroid_eq_centralizer_mulLeftRight
∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α],
(CentroidHom.toEndRingHom α).rangeS =
Subsemiring.centralizer (Set.range ⇑AddMonoid.End.mulLeft ∪ Set.range ⇑AddMonoid.End.mulRight)- Defined in
- Mathlib.Algebra.Ring.CentroidHom
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 33 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.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Set.rangestatement and proof · cited by 4,705
- AddMonoidHomstatement · cited by 3,230
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Subsemiringstatement · cited by 456
- AddMonoidHom.extproof · cited by 149
- CentroidHomstatement and proof · cited by 67
- AddMonoid.Endstatement and proof · cited by 64
- RingHom.rangeSstatement and proof · cited by 47
- Subsemiring.centralizerstatement and proof · cited by 13
- AddMonoid.End.mulLeftstatement and proof · cited by 11
Cited by1
Results whose statement or proof uses this declaration.
- NonUnitalNonAssocCommSemiring.mem_center_iffproof · cited by 0