Semiconj

📁 Source: Mathlib/Algebra/Ring/Semiconj.lean

Statistics

Metric	Count
Definitions	0
Theorems add_left, add_right, neg_left, neg_left_iff, neg_one_left, neg_one_right, neg_right, neg_right_iff, sub_left, sub_right	10
Total	10

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_left 📖	mathematical	SemiconjBy Distrib.toMul	Distrib.toAdd	—	right_distrib Distrib.rightDistribClass eq left_distrib Distrib.leftDistribClass
add_right 📖	mathematical	SemiconjBy Distrib.toMul	Distrib.toAdd	—	left_distrib Distrib.leftDistribClass eq right_distrib Distrib.rightDistribClass
neg_left 📖	mathematical	SemiconjBy	InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg	—	neg_mul eq mul_neg
neg_left_iff 📖	mathematical	—	SemiconjBy InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg	—	neg_left neg_neg
neg_one_left 📖	mathematical	—	SemiconjBy MulOne.toMul MulOneClass.toMulOne InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toOne	—	—
neg_one_right 📖	mathematical	—	SemiconjBy MulOne.toMul MulOneClass.toMulOne InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toOne	—	—
neg_right 📖	mathematical	SemiconjBy	InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg	—	mul_neg eq neg_mul
neg_right_iff 📖	mathematical	—	SemiconjBy InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg	—	neg_right neg_neg
sub_left 📖	mathematical	SemiconjBy Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	sub_eq_add_neg add_left neg_left
sub_right 📖	mathematical	SemiconjBy Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	sub_eq_add_neg add_right neg_right

---

← Back to Index