Centralizer

Statistics

Metric	Count
Definitions	0
Theorems `add_mem_centralizer`, `neg_mem_centralizer`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem_centralizer` 📖	mathematical	`Set` `instMembership` `centralizer` `Distrib.toMul`	`Set` `instMembership` `centralizer` `Distrib.toMul` `Distrib.toAdd`	—	`add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass`
`neg_mem_centralizer` 📖	mathematical	`Set` `instMembership` `centralizer`	`Set` `instMembership` `centralizer` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`mul_neg` `neg_mul`

---