Associated

Statistics

Metric	Count
Definitions	0
Theorems `neg_left`, `neg_left_iff`, `neg_neg`, `neg_right`, `neg_right_iff`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_left` 📖	mathematical	`Associated`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_neg` `neg_mul` `neg_neg`
`neg_left_iff` 📖	mathematical	—	`Associated` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`neg_left` `neg_neg`
`neg_neg` 📖	mathematical	`Associated`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`neg_right` `neg_left`
`neg_right` 📖	mathematical	`Associated`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`symm` `neg_left`
`neg_right_iff` 📖	mathematical	—	`Associated` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`neg_right` `neg_neg`

---