Units

📁 Source: Mathlib/Data/Int/Order/Units.lean

Statistics

Metric	Count
Definitions	0
Theorems isUnit_iff_abs_eq, isUnit_sq, neg_one_pow_ne_zero, sq_eq_one_of_sq_le_three, sq_eq_one_of_sq_lt_four, units_coe_mul_self, units_div_eq_mul, units_inv_eq_self, units_mul_self, units_pow_eq_pow_mod_two, units_pow_two, units_sq	12
Total	12

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_iff_abs_eq 📖	mathematical	—	IsUnit instMonoid abs instLatticeInt instAddGroup	—	isUnit_iff_natAbs_eq abs_eq_natAbs
isUnit_sq 📖	mathematical	IsUnit instMonoid	Monoid.toNatPow	—	sq isUnit_mul_self
neg_one_pow_ne_zero 📖	—	—	—	—	isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain instNontrivial
sq_eq_one_of_sq_le_three 📖	—	Monoid.toNatPow instMonoid	—	—	sq_eq_one_of_sq_lt_four lt_of_le_of_lt lt_add_one instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd instAddLeftMono
sq_eq_one_of_sq_lt_four 📖	—	Monoid.toNatPow instMonoid	—	—	sq_eq_one_iff IsDomain.to_noZeroDivisors instIsDomain abs_eq instIsOrderedAddMonoid zero_le_one' instZeroLEOneClass le_antisymm abs_lt_of_sq_lt_sq instIsStrictOrderedRing zero_le_two instAddLeftMono abs_pos
units_coe_mul_self 📖	mathematical	—	Units.val instMonoid	—	Units.val_mul units_mul_self Units.val_one
units_div_eq_mul 📖	mathematical	—	Units instMonoid Units.instDiv Units.instMul	—	div_eq_mul_inv units_inv_eq_self
units_inv_eq_self 📖	mathematical	—	Units instMonoid Units.instInv	—	inv_eq_iff_mul_eq_one units_mul_self
units_mul_self 📖	mathematical	—	Units instMonoid Units.instMul Units.instOne	—	sq units_sq
units_pow_eq_pow_mod_two 📖	mathematical	—	Units instMonoid Monoid.toNatPow Units.instMonoid	—	pow_add pow_mul units_sq one_pow mul_one
units_pow_two 📖	mathematical	—	Units instMonoid Monoid.toNatPow Units.instMonoid Units.instOne	—	units_sq
units_sq 📖	mathematical	—	Units instMonoid Monoid.toNatPow Units.instMonoid Units.instOne	—	Units.ext_iff Units.val_pow_eq_pow_val Units.val_one isUnit_sq Units.isUnit

---

← Back to Index