Theorems · Theorem · ring theory
CentroidHom.star_centerToCentroidCenter
∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] (z : ↥(NonUnitalStarSubsemiring.center α)),
star (CentroidHom.centerToCentroidCenter z) = CentroidHom.centerToCentroidCenter (star z)- Defined in
- Mathlib.Algebra.Star.CentroidHom
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- StarRingstatement and proof · cited by 1,686
- Star.starstatement and proof · cited by 1,082
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Subsemiringstatement · cited by 456
- NonUnitalSubsemiringstatement · cited by 201
- NonUnitalRingHomstatement · cited by 157
- star_starproof · cited by 135
- StarMul.star_mulproof · cited by 72
- CentroidHomstatement · cited by 67
- IsMulCentral.commproof · cited by 26
- NonUnitalSubsemiring.centerstatement · cited by 22
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.