Semiconj

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

Statistics

Metric	Count
Definitions	0
Theorems self_zpow₀, zpow_left₀, zpow_right₀, zpow_self₀, zpow_zpow_self₀, zpow_zpow₀, div_right, inv_right_iff₀, inv_right₀, inv_symm_left_iff₀, inv_symm_left₀, zero_left, zero_right, zpow_right₀	14
Total	14

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
self_zpow₀ 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_right₀ refl
zpow_left₀ 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	symm zpow_right₀
zpow_right₀ 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	SemiconjBy.zpow_right₀
zpow_self₀ 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_left₀ refl
zpow_zpow_self₀ 📖	mathematical	—	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_zpow₀ refl
zpow_zpow₀ 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_right₀ zpow_left₀

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_right 📖	mathematical	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	div_eq_mul_inv mul_right inv_right₀
inv_right_iff₀ 📖	mathematical	—	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_right₀ inv_inv
inv_right₀ 📖	mathematical	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_zero MulZeroClass.mul_zero GroupWithZero.noZeroDivisors mul_ne_zero units_inv_right mul_ne_zero_iff eq
inv_symm_left_iff₀ 📖	mathematical	—	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Classical.by_cases inv_zero units_inv_symm_left_iff
inv_symm_left₀ 📖	mathematical	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_symm_left_iff₀
zero_left 📖	mathematical	—	SemiconjBy MulZeroClass.toMul MulZeroClass.toZero	—	MulZeroClass.zero_mul MulZeroClass.mul_zero
zero_right 📖	mathematical	—	SemiconjBy MulZeroClass.toMul MulZeroClass.toZero	—	MulZeroClass.mul_zero MulZeroClass.zero_mul
zpow_right₀ 📖	mathematical	SemiconjBy MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	zpow_natCast pow_right zpow_negSucc inv_right₀

---

← Back to Index