Center

Statistics

Metric	Count
Definitions	0
Theorems `star_centralizer`, `star_mem_center`, `star_mem_centralizer`, `star_mem_centralizer'`, `union_star_self_comm`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`star_centralizer` 📖	mathematical	—	`Star.star` `Set` `InvolutiveStar.toStar` `instInvolutiveStar` `StarMul.toInvolutiveStar` `centralizer`	—	—
`star_mem_center` 📖	mathematical	`Set` `instMembership` `center`	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	`StarMul.star_mul` `star_star` `Commute.symm` `IsMulCentral.comm` `mem_center_iff` `IsMulCentral.right_assoc` `IsMulCentral.left_assoc`
`star_mem_centralizer` 📖	—	`Set` `instMembership` `centralizer` `instUnion` `Star.star` `star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	—	—	`star_mem_centralizer'` `star_mem_star`
`star_mem_centralizer'` 📖	—	`Set` `instMembership` `Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `centralizer`	—	—	`StarMul.star_mul` `star_star`
`union_star_self_comm` 📖	—	`Star.star` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Set` `instMembership` `instUnion` `instInvolutiveStar`	—	—	`centralizer_union`

---