NeZero

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

Statistics

Metric	Count
Definitions	0
Theorems one, domain_nontrivial, inv_mul_cancel₀, inv_ne_zero	4
Total	4

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one 📖	mathematical	—	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	exists_pair_ne one_mul MulZeroClass.zero_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domain_nontrivial 📖	mathematical	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	Nontrivial	—	zero_ne_one NeZero.one
inv_mul_cancel₀ 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toInv GroupWithZero.toDivInvMonoid MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_inv_cancel_right₀ inv_ne_zero mul_inv_cancel₀
inv_ne_zero 📖	—	—	—	—	MulZeroClass.mul_zero NeZero.one GroupWithZero.toNontrivial mul_inv_cancel₀

---

← Back to Index