Conj

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

Statistics

Metric	Count
Definitions	0
Theorems conj_pow₀, isConj_iff₀	2
Total	2

GroupWithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_pow₀ 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid toDivisionMonoid	—	mul_inv_cancel₀ inv_mul_cancel₀ Units.conj_pow'
isConj_iff₀ 📖	mathematical	—	IsConj MonoidWithZero.toMonoid toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid toDivisionMonoid	—	IsConj.eq_1 Units.exists_iff_ne_zero mul_inv_eq_iff_eq_mul₀

---

← Back to Index