Units

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/Units.lean

Statistics

Metric	Count
Definitions	0
Theorems le_of_mul_le_mul_left, le_of_mul_le_mul_right, mulLECancellable, mul_le_mul_left, mul_le_mul_right, inv_le_one, inv_le_one_of_le, inv_mul_le_iff, inv_mul_le_of_le_mul, inv_mul_le_one, inv_mul_le_one_of_le, le_inv_mul_iff, le_inv_mul_of_mul_le, le_mul_inv_iff, le_mul_inv_of_mul_le, le_mul_of_inv_mul_le, le_mul_of_mul_inv_le, le_of_inv_le_one, le_of_inv_mul_le_one, le_of_mul_inv_le_one, le_of_one_le_inv, le_of_one_le_inv_mul, le_of_one_le_mul_inv, mulLECancellable_val, mul_inv_le_iff, mul_inv_le_of_le_mul, mul_inv_le_one, mul_inv_le_one_of_le, mul_le_of_le_inv_mul, mul_le_of_le_mul_inv, one_le_inv, one_le_inv_mul, one_le_inv_mul_of_le, one_le_inv_of_le, one_le_mul_inv, one_le_mul_inv_of_le	36
Total	36

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_mul_le_mul_left 📖	—	IsUnit MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—	mul_le_mul_left
le_of_mul_le_mul_right 📖	—	IsUnit MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—	mul_le_mul_right
mulLECancellable 📖	mathematical	IsUnit	MulLECancellable MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Units.mulLECancellable_val
mul_le_mul_left 📖	mathematical	IsUnit	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
mul_le_mul_right 📖	mathematical	IsUnit	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_le_one 📖	mathematical	—	val Units instInv MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mul_one mul_inv
inv_le_one_of_le 📖	mathematical	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass val	Units instInv	—	inv_le_one
inv_mul_le_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	mul_inv_cancel_left
inv_mul_le_of_le_mul 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val	Units instInv	—	inv_mul_le_iff
inv_mul_le_one 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv MulOne.toOne	—	inv_mul_le_iff mul_one
inv_mul_le_one_of_le 📖	mathematical	val	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Units instInv MulOne.toOne	—	inv_mul_le_one
le_inv_mul_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	mul_inv_cancel_left
le_inv_mul_of_mul_le 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val	Units instInv	—	le_inv_mul_iff
le_mul_inv_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	inv_mul_cancel_right
le_mul_inv_of_mul_le 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val	Units instInv	—	le_mul_inv_iff
le_mul_of_inv_mul_le 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	—	inv_mul_le_iff
le_mul_of_mul_inv_le 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	—	mul_inv_le_iff
le_of_inv_le_one 📖	—	val Units instInv MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—	inv_le_one
le_of_inv_mul_le_one 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv MulOne.toOne	—	—	inv_mul_le_one
le_of_mul_inv_le_one 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv MulOne.toOne	—	—	mul_inv_le_one
le_of_one_le_inv 📖	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	—	one_le_inv
le_of_one_le_inv_mul 📖	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul val Units instInv	—	—	one_le_inv_mul
le_of_one_le_mul_inv 📖	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul val Units instInv	—	—	one_le_mul_inv
mulLECancellable_val 📖	mathematical	—	MulLECancellable MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val	—	inv_mul_cancel_left mul_le_mul_right
mul_inv_le_iff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	inv_mul_cancel_right
mul_inv_le_of_le_mul 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val	Units instInv	—	mul_inv_le_iff
mul_inv_le_one 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv MulOne.toOne	—	mul_inv_le_iff one_mul
mul_inv_le_one_of_le 📖	mathematical	val	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Units instInv MulOne.toOne	—	mul_inv_le_one
mul_le_of_le_inv_mul 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	—	le_inv_mul_iff
mul_le_of_le_mul_inv 📖	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	—	le_mul_inv_iff
one_le_inv 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass val Units instInv	—	mul_one mul_inv
one_le_inv_mul 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul val Units instInv	—	le_inv_mul_iff mul_one
one_le_inv_mul_of_le 📖	mathematical	val	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul Units instInv	—	one_le_inv_mul
one_le_inv_of_le 📖	mathematical	val MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Units instInv	—	one_le_inv
one_le_mul_inv 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul val Units instInv	—	le_mul_inv_iff one_mul
one_le_mul_inv_of_le 📖	mathematical	val	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toMul Units instInv	—	one_le_mul_inv

---

← Back to Index