Units

📁 Source: Mathlib/Algebra/Group/Int/Units.lean

Statistics

Metric	Count
Definitions	0
Theorems natAbs_eq, eq_of_mul_eq_one, eq_one_or_neg_one_of_mul_eq_neg_one, eq_one_or_neg_one_of_mul_eq_neg_one', eq_one_or_neg_one_of_mul_eq_one, eq_one_or_neg_one_of_mul_eq_one', isUnit_add_isUnit_eq_isUnit_add_isUnit, isUnit_eq_one_or, isUnit_eq_or_eq_neg, isUnit_iff, isUnit_iff_natAbs_eq, isUnit_mul_self, isUnit_ne_iff_eq_neg, mul_eq_neg_one_iff_eq_one_or_neg_one, mul_eq_one_iff_eq_one_or_neg_one, natAbs_of_isUnit, ofNat_isUnit, units_natAbs	18
Total	18

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_mul_eq_one 📖	—	—	—	—	eq_one_or_neg_one_of_mul_eq_one'
eq_one_or_neg_one_of_mul_eq_neg_one 📖	—	—	—	—	eq_one_or_neg_one_of_mul_eq_neg_one'
eq_one_or_neg_one_of_mul_eq_neg_one' 📖	—	—	—	—	isUnit_eq_one_or IsUnit.mul_iff instIsDedekindFiniteMonoid isUnit_iff one_mul
eq_one_or_neg_one_of_mul_eq_one 📖	—	—	—	—	isUnit_iff IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid
eq_one_or_neg_one_of_mul_eq_one' 📖	—	—	—	—	mul_comm eq_one_or_neg_one_of_mul_eq_one
isUnit_add_isUnit_eq_isUnit_add_isUnit 📖	—	IsUnit instMonoid	—	—	isUnit_iff
isUnit_eq_one_or 📖	—	IsUnit instMonoid	—	—	natAbs_of_isUnit
isUnit_eq_or_eq_neg 📖	—	IsUnit instMonoid	—	—	isUnit_ne_iff_eq_neg
isUnit_iff 📖	mathematical	—	IsUnit instMonoid	—	isUnit_eq_one_or isUnit_one
isUnit_iff_natAbs_eq 📖	mathematical	—	IsUnit instMonoid	—	—
isUnit_mul_self 📖	—	IsUnit instMonoid	—	—	isUnit_eq_one_or
isUnit_ne_iff_eq_neg 📖	—	IsUnit instMonoid	—	—	isUnit_eq_one_or
mul_eq_neg_one_iff_eq_one_or_neg_one 📖	—	—	—	—	eq_one_or_neg_one_of_mul_eq_neg_one'
mul_eq_one_iff_eq_one_or_neg_one 📖	—	—	—	—	eq_one_or_neg_one_of_mul_eq_one'
natAbs_of_isUnit 📖	—	IsUnit instMonoid	—	—	units_natAbs
ofNat_isUnit 📖	mathematical	—	IsUnit instMonoid Nat.instMonoid	—	Unique.instSubsingleton
units_natAbs 📖	mathematical	—	Units.val instMonoid	—	Units.mul_inv Units.inv_mul Units.ext_iff Nat.units_eq_one

Int.IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natAbs_eq 📖	—	IsUnit Int.instMonoid	—	—	Int.isUnit_iff_natAbs_eq

---

← Back to Index