Defs

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

Statistics

Metric	Count
Definitions `AddCommute`	1
Theorems `addSemiconjBy`, `add_add_add_comm`, `add_left`, `add_neg`, `add_neg_cancel`, `add_neg_cancel_assoc`, `add_nsmul`, `add_right`, `all`, `eq`, `instRefl`, `left_comm`, `neg`, `nsmul_left`, `nsmul_nsmul`, `nsmul_nsmul_self`, `nsmul_right`, `nsmul_self`, `on_refl`, `refl`, `right_comm`, `self_nsmul`, `symm_iff`, `zero_left`, `zero_right`, `zsmul_add`, `all`, `eq`, `instRefl`, `inv`, `left_comm`, `mul_inv`, `mul_inv_cancel`, `mul_inv_cancel_assoc`, `mul_left`, `mul_mul_mul_comm`, `mul_pow`, `mul_right`, `mul_zpow`, `on_refl`, `one_left`, `one_right`, `pow_left`, `pow_pow`, `pow_pow_self`, `pow_right`, `pow_self`, `refl`, `right_comm`, `self_pow`, `semiconjBy`, `symm_iff`, `addCommute_iff_eq`, `commute_iff_eq`	54
Total	55

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSemiconjBy` 📖	mathematical	`AddCommute`	`AddSemiconjBy`	—	—
`add_add_add_comm` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`AddSemigroup.toAdd`	—	`add_assoc` `left_comm`
`add_left` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`AddCommute` `AddSemigroup.toAdd`	—	`AddSemiconjBy.add_left`
`add_neg` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`SubNegMonoid.toNeg` `SubtractionMonoid.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`eq` `neg_add_rev`
`add_neg_cancel` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toNeg`	—	`eq` `add_neg_cancel_right`
`add_neg_cancel_assoc` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SubNegMonoid.toNeg`	—	`add_assoc` `add_neg_cancel`
`add_nsmul` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`zero_nsmul` `zero_add` `succ_nsmul'` `add_assoc` `right_comm` `nsmul_left`
`add_right` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`AddCommute` `AddSemigroup.toAdd`	—	`AddSemiconjBy.add_right`
`all` 📖	mathematical	—	`AddCommute` `AddCommMagma.toAdd`	—	`add_comm`
`eq` 📖	—	`AddCommute`	—	—	—
`instRefl` 📖	mathematical	—	`AddCommute`	—	`refl`
`left_comm` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`AddSemigroup.toAdd`	—	`add_assoc` `eq`
`neg` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`SubNegMonoid.toNeg` `SubtractionMonoid.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`eq` `neg_add_rev`
`nsmul_left` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`symm` `nsmul_right`
`nsmul_nsmul` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul_right` `nsmul_left`
`nsmul_nsmul_self` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul_nsmul` `refl`
`nsmul_right` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`AddSemiconjBy.nsmul_right`
`nsmul_self` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul_left` `refl`
`on_refl` 📖	mathematical	—	`AddCommute`	—	`refl`
`refl` 📖	mathematical	—	`AddCommute`	—	—
`right_comm` 📖	mathematical	`AddCommute` `AddSemigroup.toAdd`	`AddSemigroup.toAdd`	—	`add_assoc` `eq`
`self_nsmul` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul_right` `refl`
`symm_iff` 📖	mathematical	—	`AddCommute`	—	`symm`
`zero_left` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`AddSemiconjBy.zero_left`
`zero_right` 📖	mathematical	—	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`AddSemiconjBy.zero_right`
`zsmul_add` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`SubNegMonoid.toZSMul` `SubtractionMonoid.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`natCast_zsmul` `add_nsmul` `negSucc_zsmul` `eq` `nsmul_nsmul` `neg_add_rev`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all` 📖	mathematical	—	`Commute` `CommMagma.toMul`	—	`mul_comm`
`eq` 📖	—	`Commute`	—	—	—
`instRefl` 📖	mathematical	—	`Commute`	—	`refl`
`inv` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`eq` `mul_inv_rev`
`left_comm` 📖	mathematical	`Commute` `Semigroup.toMul`	`Semigroup.toMul`	—	`eq`
`mul_inv` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`eq` `mul_inv_rev`
`mul_inv_cancel` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toInv`	—	`eq` `mul_inv_cancel_right`
`mul_inv_cancel_assoc` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toInv`	—	`mul_assoc` `mul_inv_cancel`
`mul_left` 📖	mathematical	`Commute` `Semigroup.toMul`	`Commute` `Semigroup.toMul`	—	`SemiconjBy.mul_left`
`mul_mul_mul_comm` 📖	mathematical	`Commute` `Semigroup.toMul`	`Semigroup.toMul`	—	`mul_assoc` `left_comm`
`mul_pow` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toPow` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_zero` `one_mul` `pow_succ'` `right_comm` `pow_left`
`mul_right` 📖	mathematical	`Commute` `Semigroup.toMul`	`Commute` `Semigroup.toMul`	—	`SemiconjBy.mul_right`
`mul_zpow` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`zpow_natCast` `mul_pow` `zpow_negSucc` `eq` `pow_pow` `mul_inv_rev`
`on_refl` 📖	mathematical	—	`Commute`	—	`refl`
`one_left` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`SemiconjBy.one_left`
`one_right` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`SemiconjBy.one_right`
`pow_left` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`symm` `pow_right`
`pow_pow` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	—
`pow_pow_self` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_pow` `refl`
`pow_right` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`SemiconjBy.pow_right`
`pow_self` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_left` `refl`
`refl` 📖	mathematical	—	`Commute`	—	—
`right_comm` 📖	mathematical	`Commute` `Semigroup.toMul`	`Semigroup.toMul`	—	`mul_assoc` `eq`
`self_pow` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow_right` `refl`
`semiconjBy` 📖	mathematical	`Commute`	`SemiconjBy`	—	—
`symm_iff` 📖	mathematical	—	`Commute`	—	`symm`

(root)

Definitions

Name	Category	Theorems
`AddCommute` 📖	MathDef	90 math math: `Multiset.noncommSum_cons'`, `AddCommute.unop`, `AddOpposite.addCommute_op`, `Finset.noncommSum_add_distrib_aux`, `AddCommute.self_nsmul`, `AddMonoidHom.noncommPiCoprod_apply`, `Pi.addCommute_iff`, `AddCommute.list_sum_right`, `AddCommute.map`, `AddUnits.addCommute_iff_neg_add_cancel_assoc`, `AddCommute.vadd_left`, `AddCommute.symm`, `Finset.noncommSum_union_of_disjoint`, `OrderAddMonoidHom.addCommute_inlₗ_inrₗ`, `AddCommute.addConj_iff`, `AddCommute.zsmul_left`, `AddCommute.prod`, `addCommute_iff_eq`, `AddCommute.addUnits_of_val`, `AddCommute.vadd_right`, `Finset.noncommSum_addCommute`, `OrderAddMonoidHom.addCommute_inl_inr`, `AddUnits.addCommute_coe_neg`, `AddCommute.symm_iff`, `AddCommute.neg_right`, `AddCommute.addUnits_val_iff`, `AddSubgroup.addCommute_subtype_of_addCommute`, `AddCommute.self_zsmul`, `AddCommute.add_left`, `Multiset.map_noncommSum_aux`, `AddCommute.zsmul_self`, `AddCommute.of_addOrderOf_dvd_two`, `AddCommute.of_map`, `AddCommute.nsmul_nsmul_self`, `AddCommute.addUnits_neg_left_iff`, `AddCommute.add_right`, `AddCommute.addUnits_zsmul_right`, `AddCommute.nsmul_nsmul`, `Finset.noncommSum_insert_of_notMem`, `Finsupp.addCommute_of_disjoint`, `AddMonoidHom.addCommute_noncommPiCoprod`, `AddUnits.addCommute_iff_add_neg_cancel_assoc`, `Finset.noncommSum_insert_of_notMem'`, `Finset.noncommSum_cons`, `AddCommute.op`, `AddCommute.addConj`, `AddUnits.addCommute_iff_neg_add_cancel`, `AddCommute.refl`, `AddCommute.nsmul_self`, `Pi.single_apply_addCommute`, `AddCommute.zsmul_zsmul`, `AddCommute.zsmul_zsmul_self`, `AddCommute.neg_neg`, `AddCommute.neg_right_iff`, `AddSubgroup.addCommute_of_normal_of_disjoint`, `AddCommute.neg_left_iff`, `addCommutatorElement_eq_zero_iff_addCommute`, `AddCommute.addUnits_zsmul_left`, `AddCommute.zero_right`, `Multiset.noncommSum_add`, `AddCommute.nsmul_right`, `Multiset.noncommSum_addCommute`, `AddMonoidHom.addCommute_inl_inr`, `AddCommute.neg_neg_iff`, `AddCommute.addUnits_neg_left`, `Finset.map_noncommSum`, `Finsupp.addCommute_iff_inter`, `AddCommute.all`, `AddCommute.addUnits_neg_right_iff`, `IsAddCentral.comm`, `AddCommute.list_sum_left`, `AddCommute.on_refl`, `AddCommute.addUnits_val`, `Finset.noncommSum_cons'`, `Multiset.noncommSum_cons`, `Prod.addCommute_iff`, `AddCommute.zero_left`, `addCommute_map_iff`, `AddUnits.addCommute_iff_add_neg_cancel`, `AddCommute.nsmul_left`, `isAddCentral_iff`, `AddCommute.instRefl`, `Finset.noncommSum_lemma`, `AddCommute.pi`, `AddCommute.zsmul_right`, `AddCommute.neg_left`, `AddUnits.addCommute_neg_coe`, `AddOpposite.addCommute_unop`, `AddCommute.addUnits_neg_right`, `AddAction.not_addCommute_of_disjoint_movedBy_preimage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommute_iff_eq` 📖	mathematical	—	`AddCommute`	—	—
`commute_iff_eq` 📖	mathematical	—	`Commute`	—	—

---

← Back to Index