Documentation Verification Report

Nat

📁 Source: Mathlib/Algebra/GCDMonoid/Nat.lean

Statistics

Metric	Count
Definitions `instGCDMonoid`, `instNormalizedGCDMonoid`, `normalizationMonoid`, `associatesIntEquivNat`, `instGCDMonoidNat`, `instNormalizedGCDMonoidNat`	6
Theorems `abs_eq_normalize`, `associated_iff`, `associated_iff_natAbs`, `associated_natAbs`, `coe_gcd`, `coe_lcm`, `eq_of_associated_of_nonneg`, `exists_unit_of_abs`, `gcd_eq_natAbs`, `natAbs_gcd`, `natAbs_lcm`, `nonneg_iff_normalize_eq_self`, `nonneg_of_normalize_eq_self`, `normUnit_eq`, `normalize_coe_nat`, `normalize_of_nonneg`, `normalize_of_nonpos`, `gcd_eq_nat_gcd`, `lcm_eq_nat_lcm`	19
Total	25

Int

Definitions

Name	Category	Theorems
`instGCDMonoid` 📖	CompOp	4 math math: `coe_gcd`, `natAbs_gcd`, `coe_lcm`, `natAbs_lcm`
`instNormalizedGCDMonoid` 📖	CompOp	—
`normalizationMonoid` 📖	CompOp	6 math math: `normalize_of_nonneg`, `normUnit_eq`, `normalize_coe_nat`, `normalize_of_nonpos`, `abs_eq_normalize`, `nonneg_iff_normalize_eq_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_eq_normalize` 📖	mathematical	—	`abs` `instLatticeInt` `instAddGroup` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	`le_total` `abs_of_nonneg` `instAddLeftMono` `normalize_of_nonneg` `abs_of_nonpos` `normalize_of_nonpos`
`associated_iff` 📖	mathematical	—	`Associated` `instMonoid`	—	`associated_iff_natAbs`
`associated_iff_natAbs` 📖	mathematical	—	`Associated` `instMonoid`	—	`dvd_dvd_iff_associated` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Nat.instIsCancelMulZero` `associated_iff_eq` `Unique.instSubsingleton`
`associated_natAbs` 📖	mathematical	—	`Associated` `instMonoid`	—	`associated_of_dvd_dvd` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `dvd_natCast` `dvd_rfl`
`coe_gcd` 📖	mathematical	—	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`coe_lcm` 📖	mathematical	—	`GCDMonoid.lcm` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`eq_of_associated_of_nonneg` 📖	—	`Associated` `instMonoid`	—	—	`dvd_antisymm_of_normalize_eq` `instIsCancelMulZero` `normalize_of_nonneg` `Associated.dvd` `Associated.symm`
`exists_unit_of_abs` 📖	—	—	—	—	`isUnit_one` `one_mul` `IsUnit.neg` `neg_eq_iff_eq_neg` `neg_mul`
`gcd_eq_natAbs` 📖	—	—	—	—	—
`natAbs_gcd` 📖	mathematical	—	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`natAbs_lcm` 📖	mathematical	—	`GCDMonoid.lcm` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`nonneg_iff_normalize_eq_self` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	`nonneg_of_normalize_eq_self` `normalize_of_nonneg`
`nonneg_of_normalize_eq_self` 📖	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	—	`normalize_of_nonpos` `LT.lt.le`
`normUnit_eq` 📖	mathematical	—	`NormalizationMonoid.normUnit` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	—
`normalize_coe_nat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	`normalize_of_nonneg` `ofNat_le_ofNat_of_le`
`normalize_of_nonneg` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	`normalize_apply` `normUnit_eq` `Units.val_one` `mul_one`
`normalize_of_nonpos` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `normalizationMonoid`	—	`LE.le.eq_or_lt` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `neg_zero` `normalize_apply` `normUnit_eq` `not_le_of_gt` `Units.val_neg` `Units.val_one` `mul_neg_one`

(root)

Definitions

Name	Category	Theorems
`associatesIntEquivNat` 📖	CompOp	—
`instGCDMonoidNat` 📖	CompOp	9 math math: `Ideal.absNorm_span_insert`, `DihedralGroup.exponent`, `gcd_eq_nat_gcd`, `AddMonoid.exponent_prod`, `UnitAddCircle.mem_approxAddOrderOf_iff`, `Monoid.exponent_prod`, `lcm_eq_nat_lcm`, `UnitAddCircle.mem_addWellApproximable_iff`, `QuaternionGroup.exponent`
`instNormalizedGCDMonoidNat` 📖	CompOp	14 math math: `Pi.addOrderOf`, `Monoid.exponent_pi`, `AddMonoid.exponent_pi`, `Function.minimalPeriod_piMap_fintype`, `Monoid.lcm_orderOf_eq_exponent`, `Monoid.lcm_orderOf_dvd_exponent`, `Equiv.Perm.lcm_cycleType`, `Finset.lcm_eq_prod`, `Pi.orderOf`, `ArithmeticFunction.carmichael_finset_lcm`, `ArithmeticFunction.carmichael_finset_prod`, `AddMonoid.lcm_addOrderOf_eq_exponent`, `ArithmeticFunction.carmichael_factorization`, `AddMonoid.lcm_addOrderOf_dvd_exponent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gcd_eq_nat_gcd` 📖	mathematical	—	`GCDMonoid.gcd` `Nat.instCommMonoidWithZero` `instGCDMonoidNat`	—	—
`lcm_eq_nat_lcm` 📖	mathematical	—	`GCDMonoid.lcm` `Nat.instCommMonoidWithZero` `instGCDMonoidNat`	—	—

---

← Back to Index