Commute

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

Statistics

Metric	Count
Definitions `instBracket`	1
Theorems `add_left`, `add_right`, `add_sq`, `lie_eq`, `mul_self_eq_mul_self_iff`, `mul_self_sub_mul_self_eq`, `mul_self_sub_mul_self_eq'`, `neg_left`, `neg_left_iff`, `neg_one_left`, `neg_one_right`, `neg_right`, `neg_right_iff`, `sq_eq_sq_iff_eq_or_eq_neg`, `sq_sub_sq`, `sub_left`, `sub_right`, `sub_sq`, `lie_def`, `eq_or_eq_neg_of_sq_eq_sq`, `inv_eq_self_iff`, `sq_eq_sq_iff_eq_or_eq_neg`, `commute_iff_lie_eq`, `eq_or_eq_neg_of_sq_eq_sq`, `mul_neg_one_pow_eq_zero_iff`, `mul_self_eq_mul_self_iff`, `mul_self_eq_one_iff`, `mul_self_sub_mul_self`, `mul_self_sub_one`, `neg_one_pow_eq_or`, `neg_one_pow_eq_pow_mod_two`, `neg_one_pow_mul_eq_zero_iff`, `neg_one_pow_two`, `neg_one_sq`, `neg_pow`, `neg_pow'`, `neg_pow_two`, `neg_sq`, `pow_two_sub_pow_two`, `sq_eq_one_iff`, `sq_eq_sq_iff_eq_or_eq_neg`, `sq_ne_one_iff`, `sq_sub_sq`, `sub_pow_two`, `sub_sq`, `sub_sq'`, `sub_sq_comm`	47
Total	48

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`Commute` `Distrib.toMul`	`Distrib.toAdd`	—	`SemiconjBy.add_left`
`add_right` 📖	mathematical	`Commute` `Distrib.toMul`	`Distrib.toAdd`	—	`SemiconjBy.add_right`
`add_sq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sq` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `eq` `add_assoc` `two_mul`
`lie_eq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`Bracket.bracket` `Ring.instBracket` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_eq_zero_of_eq`
`mul_self_eq_mul_self_iff` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	`sub_eq_zero` `mul_self_sub_mul_self_eq` `mul_eq_zero` `add_eq_zero_iff_eq_neg`
`mul_self_sub_mul_self_eq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd`	—	`add_mul` `Distrib.rightDistribClass` `mul_sub` `eq` `sub_add_sub_cancel`
`mul_self_sub_mul_self_eq'` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd`	—	`mul_add` `Distrib.leftDistribClass` `sub_mul` `eq` `sub_add_sub_cancel`
`neg_left` 📖	mathematical	`Commute`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`SemiconjBy.neg_left`
`neg_left_iff` 📖	mathematical	—	`Commute` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`SemiconjBy.neg_left_iff`
`neg_one_left` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toOne`	—	`SemiconjBy.neg_one_left`
`neg_one_right` 📖	mathematical	—	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toOne`	—	`SemiconjBy.neg_one_right`
`neg_right` 📖	mathematical	`Commute`	`InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`SemiconjBy.neg_right`
`neg_right_iff` 📖	mathematical	—	`Commute` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	`SemiconjBy.neg_right_iff`
`sq_eq_sq_iff_eq_or_eq_neg` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`sub_eq_zero` `sq_sub_sq` `mul_eq_zero` `add_eq_zero_iff_eq_neg`
`sq_sub_sq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd`	—	`sq` `mul_self_sub_mul_self_eq`
`sub_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`SemiconjBy.sub_left`
`sub_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`SemiconjBy.sub_right`
`sub_sq` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sq` `mul_sub` `sub_mul` `eq` `two_mul` `add_mul` `Distrib.rightDistribClass`

Ring

Definitions

Name	Category	Theorems
`instBracket` 📖	CompOp	10 math math: `Commute.lie_eq`, `RootPairing.GeckConstruction.lie_h_e`, `RootPairing.GeckConstruction.lie_e_f_same`, `RootPairing.GeckConstruction.lie_h_f`, `lie_def`, `RootPairing.GeckConstruction.lie_h_h`, `commute_iff_lie_eq`, `RootPairing.GeckConstruction.lie_e_f_mul_ω`, `RootPairing.GeckConstruction.lie_e_f_ne`, `LinearMap.trace_lie`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lie_def` 📖	mathematical	—	`Bracket.bracket` `instBracket` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_eq_neg_of_sq_eq_sq` 📖	mathematical	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `instMonoid`	`instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`sq_eq_sq_iff_eq_or_eq_neg`
`inv_eq_self_iff` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `instInv` `instOne` `instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`inv_eq_iff_mul_eq_one` `mul_self_eq_one_iff`
`sq_eq_sq_iff_eq_or_eq_neg` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `instMonoid` `instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_iff_lie_eq` 📖	mathematical	—	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Bracket.bracket` `Ring.instBracket` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_eq_zero`
`eq_or_eq_neg_of_sq_eq_sq` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`sq_eq_sq_iff_eq_or_eq_neg`
`mul_neg_one_pow_eq_zero_iff` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`neg_one_pow_eq_or` `mul_one` `mul_neg`
`mul_self_eq_mul_self_iff` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	`Commute.mul_self_eq_mul_self_iff` `Commute.all`
`mul_self_eq_one_iff` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	`Commute.mul_self_eq_mul_self_iff` `Commute.one_right` `mul_one`
`mul_self_sub_mul_self` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toAdd`	—	`Commute.mul_self_sub_mul_self_eq` `Commute.all`
`mul_self_sub_one` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd`	—	`Commute.mul_self_sub_mul_self_eq` `Commute.one_right` `mul_one`
`neg_one_pow_eq_or` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`pow_zero` `pow_succ` `neg_one_mul` `neg_neg` `one_mul`
`neg_one_pow_eq_pow_mod_two` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`pow_add` `pow_mul` `sq` `mul_neg` `mul_one` `neg_neg` `one_pow`
`neg_one_pow_mul_eq_zero_iff` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`neg_one_pow_eq_or` `one_mul` `neg_mul`
`neg_one_pow_two` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`neg_one_sq`
`neg_one_sq` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`neg_sq` `one_pow`
`neg_pow` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Commute.mul_pow` `Commute.neg_one_left` `neg_one_mul`
`neg_pow'` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`Commute.mul_pow` `Commute.neg_one_right` `mul_neg_one`
`neg_pow_two` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`neg_sq`
`neg_sq` 📖	mathematical	—	`Monoid.toNatPow` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`sq` `mul_neg` `neg_mul` `neg_neg`
`pow_two_sub_pow_two` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd`	—	`sq_sub_sq`
`sq_eq_one_iff` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Commute.sq_eq_sq_iff_eq_or_eq_neg` `Commute.one_right` `one_pow`
`sq_eq_sq_iff_eq_or_eq_neg` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`Commute.sq_eq_sq_iff_eq_or_eq_neg` `Commute.all`
`sq_ne_one_iff` 📖	—	—	—	—	`Iff.not` `sq_eq_one_iff`
`sq_sub_sq` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd`	—	`Commute.sq_sub_sq` `Commute.all`
`sub_pow_two` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`sub_sq`
`sub_sq` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `add_sq` `neg_sq` `mul_neg`
`sub_sq'` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `add_sq'` `neg_sq` `mul_neg`
`sub_sq_comm` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_sq'` `mul_right_comm` `add_comm`

---

← Back to Index