Commute

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

Statistics

Metric	Count
Definitions	0
Theorems div_left, div_right, inv_left_iff₀, inv_left₀, inv_right_iff₀, inv_right₀, ringInverse_ringInverse, zero_left, zero_right, inverse_pow, inverse_pow_mul_eq_iff_eq_mul, mul_inverse_rev, mul_inverse_rev', pow_inv_comm₀	14
Total	14

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_left 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	div_eq_mul_inv mul_left inv_left₀
div_right 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	SemiconjBy.div_right
inv_left_iff₀ 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	SemiconjBy.inv_symm_left_iff₀
inv_left₀ 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_left_iff₀
inv_right_iff₀ 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	SemiconjBy.inv_right_iff₀
inv_right₀ 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_right_iff₀
ringInverse_ringInverse 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	Ring.inverse	—	Ring.mul_inverse_rev' symm eq
zero_left 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroClass.toZero	—	SemiconjBy.zero_left
zero_right 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroClass.toZero	—	SemiconjBy.zero_right

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid inverse	—	pow_zero inverse_one pow_succ' pow_succ mul_inverse_rev' Commute.pow_left Commute.refl
inverse_pow_mul_eq_iff_eq_mul 📖	mathematical	IsUnit MonoidWithZero.toMonoid	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow inverse	—	inverse_pow inverse_mul_eq_iff_eq_mul IsUnit.pow
mul_inverse_rev 📖	mathematical	—	inverse CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	mul_inverse_rev' Commute.all
mul_inverse_rev' 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	inverse	—	Commute.isUnit_mul_iff Units.val_mul inverse_unit mul_inv_rev not_and_or inverse_non_unit MulZeroClass.mul_zero MulZeroClass.zero_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_inv_comm₀ 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Monoid.toNatPow MonoidWithZero.toMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Commute.pow_pow Commute.inv_left₀ Commute.refl

---

← Back to Index