Documentation Verification Report

Units

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

Statistics

Metric	Count
Definitions `unique_addUnits`, `unique_units`	2
Theorems `addUnits_eq_zero`, `isAddUnit_iff`, `isUnit_iff`, `units_eq_one`	4
Total	6

Nat

Definitions

Name	Category	Theorems
`unique_addUnits` 📖	CompOp	—
`unique_units` 📖	CompOp	10 math math: `factors_multiset_prod_of_irreducible`, `two_le_radical_iff`, `radical_pos`, `factors_eq`, `radical_le_self_iff`, `sum_divisors_filter_squarefree`, `UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors`, `one_lt_radical_iff`, `divisors_filter_squarefree`, `radical_le_one_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addUnits_eq_zero` 📖	mathematical	—	`AddUnits` `instAddMonoid` `AddUnits.instZero`	—	`AddUnits.ext` `AddUnits.val_neg`
`isAddUnit_iff` 📖	mathematical	—	`IsAddUnit` `instAddMonoid`	—	`isAddUnit_iff_eq_zero` `Unique.instSubsingleton`
`isUnit_iff` 📖	mathematical	—	`IsUnit` `instMonoid`	—	`isUnit_iff_eq_one` `Unique.instSubsingleton`
`units_eq_one` 📖	mathematical	—	`Units` `instMonoid` `Units.instOne`	—	`Units.ext` `Units.val_inv`

---

← Back to Index