Basic

📁 Source: Mathlib/Algebra/Group/Semiconj/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems eq_zero_iff, neg_neg_symm, neg_neg_symm_iff, neg_right, neg_right_iff, neg_symm_left, neg_symm_left_iff, zsmul_right, eq_one_iff, inv_inv_symm, inv_inv_symm_iff, inv_right, inv_right_iff, inv_symm_left, inv_symm_left_iff, zpow_right	16
Total	16

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	conj_eq_zero_iff eq add_neg_cancel_right
neg_neg_symm 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SubtractionMonoid.toSubNegMonoid	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	—	neg_neg_symm_iff
neg_neg_symm_iff 📖	mathematical	—	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SubtractionMonoid.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	—	neg_add_rev
neg_right 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_right_iff
neg_right_iff 📖	mathematical	—	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_symm_left_iff neg_neg_symm_iff
neg_symm_left 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_symm_left_iff
neg_symm_left_iff 📖	mathematical	—	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_add_neg_iff_add_eq add_assoc neg_add_eq_iff_eq_add
zsmul_right 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	SubNegMonoid.toZSMul	—	natCast_zsmul nsmul_right negSucc_zsmul neg_right_iff

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one_iff 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	conj_eq_one_iff eq mul_inv_cancel_right
inv_inv_symm 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid DivisionMonoid.toDivInvMonoid	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid	—	inv_inv_symm_iff
inv_inv_symm_iff 📖	mathematical	—	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid DivisionMonoid.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid	—	—
inv_right 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_right_iff
inv_right_iff 📖	mathematical	—	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_symm_left_iff inv_inv_symm_iff
inv_symm_left 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_symm_left_iff
inv_symm_left_iff 📖	mathematical	—	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mul_assoc
zpow_right 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	DivInvMonoid.toZPow	—	zpow_natCast pow_right zpow_negSucc

---

← Back to Index