Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `add_sub_add_comm`, `conj`, `conj_iff`, `function_commute_add_left`, `function_commute_add_right`, `neg_add_cancel`, `neg_add_cancel_assoc`, `neg_left`, `neg_left_iff`, `neg_neg`, `neg_neg_iff`, `neg_right`, `neg_right_iff`, `self_zsmul`, `sub_add_sub_comm`, `sub_sub_sub_comm`, `zsmul_left`, `zsmul_right`, `zsmul_self`, `zsmul_zsmul`, `zsmul_zsmul_self`, `function_semiconj_add_left`, `function_semiconj_add_right_swap`, `conj`, `conj_iff`, `div_div_div_comm`, `div_mul_div_comm`, `function_commute_mul_left`, `function_commute_mul_right`, `inv_inv`, `inv_inv_iff`, `inv_left`, `inv_left_iff`, `inv_mul_cancel`, `inv_mul_cancel_assoc`, `inv_right`, `inv_right_iff`, `mul_div_mul_comm`, `self_zpow`, `zpow_left`, `zpow_right`, `zpow_self`, `zpow_zpow`, `zpow_zpow_self`, `function_semiconj_mul_left`, `function_semiconj_mul_right_swap`, `nsmul_neg_comm`, `pow_inv_comm`	48
Total	48

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sub_add_comm` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`SubNegMonoid.toSub`	—	`sub_add_sub_comm` `symm`
`conj` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`conj_iff`
`conj_iff` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddSemiconjBy.conj_iff`
`function_commute_add_left` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`Function.Commute`	—	`AddSemiconjBy.function_semiconj_add_left`
`function_commute_add_right` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`Function.Commute`	—	`AddSemiconjBy.function_semiconj_add_right_swap`
`neg_add_cancel` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`eq` `neg_left` `neg_add_cancel_right`
`neg_add_cancel_assoc` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_assoc` `neg_add_cancel`
`neg_left` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_left_iff`
`neg_left_iff` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddSemiconjBy.neg_symm_left_iff`
`neg_neg` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`AddSemiconjBy.neg_neg_symm`
`neg_neg_iff` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`AddSemiconjBy.neg_neg_symm_iff`
`neg_right` 📖	mathematical	`AddCommute` `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	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddSemiconjBy.neg_right_iff`
`self_zsmul` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toZSMul`	—	`zsmul_right` `refl`
`sub_add_sub_comm` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg` `neg_add_rev` `eq` `symm` `neg_neg` `add_add_add_comm`
`sub_sub_sub_comm` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg` `neg_add_rev` `neg_neg` `eq` `symm` `add_add_add_comm` `neg_neg`
`zsmul_left` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`SubNegMonoid.toZSMul`	—	`symm` `zsmul_right`
`zsmul_right` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`SubNegMonoid.toZSMul`	—	`AddSemiconjBy.zsmul_right`
`zsmul_self` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toZSMul`	—	`zsmul_left` `refl`
`zsmul_zsmul` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`SubNegMonoid.toZSMul`	—	`zsmul_right` `zsmul_left`
`zsmul_zsmul_self` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toZSMul`	—	`zsmul_zsmul` `refl`

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`function_semiconj_add_left` 📖	mathematical	`AddSemiconjBy` `AddSemigroup.toAdd`	`Function.Semiconj`	—	`add_assoc` `eq`
`function_semiconj_add_right_swap` 📖	mathematical	`AddSemiconjBy` `AddSemigroup.toAdd`	`Function.Semiconj`	—	`add_assoc` `eq`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`conj_iff`
`conj_iff` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`SemiconjBy.conj_iff`
`div_div_div_comm` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	`DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_inv_rev` `inv_inv` `eq` `symm` `mul_mul_mul_comm` `inv_inv`
`div_mul_div_comm` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	`DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_inv_rev` `eq` `symm` `inv_inv` `mul_mul_mul_comm`
`function_commute_mul_left` 📖	mathematical	`Commute` `Semigroup.toMul`	`Function.Commute`	—	`SemiconjBy.function_semiconj_mul_left`
`function_commute_mul_right` 📖	mathematical	`Commute` `Semigroup.toMul`	`Function.Commute`	—	`SemiconjBy.function_semiconj_mul_right_swap`
`inv_inv` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`SemiconjBy.inv_inv_symm`
`inv_inv_iff` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`SemiconjBy.inv_inv_symm_iff`
`inv_left` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_left_iff`
`inv_left_iff` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`SemiconjBy.inv_symm_left_iff`
`inv_mul_cancel` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`eq` `inv_left` `inv_mul_cancel_right`
`inv_mul_cancel_assoc` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_assoc` `inv_mul_cancel`
`inv_right` 📖	mathematical	`Commute` `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	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`SemiconjBy.inv_right_iff`
`mul_div_mul_comm` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	`DivInvMonoid.toDiv`	—	`div_mul_div_comm` `symm`
`self_zpow` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`zpow_right` `refl`
`zpow_left` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DivInvMonoid.toZPow`	—	`symm` `zpow_right`
`zpow_right` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DivInvMonoid.toZPow`	—	`SemiconjBy.zpow_right`
`zpow_self` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`zpow_left` `refl`
`zpow_zpow` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DivInvMonoid.toZPow`	—	`zpow_right` `zpow_left`
`zpow_zpow_self` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`zpow_zpow` `refl`

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`function_semiconj_mul_left` 📖	mathematical	`SemiconjBy` `Semigroup.toMul`	`Function.Semiconj`	—	`eq`
`function_semiconj_mul_right_swap` 📖	mathematical	`SemiconjBy` `Semigroup.toMul`	`Function.Semiconj`	—	`mul_assoc` `eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_neg_comm` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toNatSMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddCommute.nsmul_nsmul` `AddCommute.neg_left` `AddCommute.refl`
`pow_inv_comm` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toNatPow` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Commute.pow_pow` `Commute.inv_left` `Commute.refl`

---

← Back to Index