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`, `gcd_nonneg`, `lcm_nonneg`, `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`	21
Total	27

Int

Definitions

Name	Category	Theorems
`instGCDMonoid` 📖	CompOp	6 math math: `gcd_nonneg`, `coe_gcd`, `natAbs_gcd`, `coe_lcm`, `natAbs_lcm`, `lcm_nonneg`
`instNormalizedGCDMonoid` 📖	CompOp	1 math math: `Finset.Int.finsetGcd_nonneg`
`normalizationMonoid` 📖	CompOp	15 math math: `normalize_of_nonneg`, `radical_eq_one_iff`, `normUnit_eq`, `two_le_radical_iff`, `UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs`, `radical_natCast`, `normalize_coe_nat`, `radical_pos`, `normalize_of_nonpos`, `abs_eq_normalize`, `radical_le_one_iff`, `radical_eq_prod_primeFactors`, `one_lt_radical_iff`, `radical_natAbs_eq_radical`, `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` 📖	mathematical	—	`IsUnit` `instMonoid`	—	`isUnit_one` `one_mul` `IsUnit.neg` `neg_eq_iff_eq_neg` `neg_mul`
`gcd_eq_natAbs` 📖	—	—	—	—	—
`gcd_nonneg` 📖	mathematical	—	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`lcm_nonneg` 📖	mathematical	—	`GCDMonoid.lcm` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `instGCDMonoid`	—	—
`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	25 math math: `Pi.addOrderOf`, `Nat.two_le_radical_iff`, `Monoid.exponent_pi`, `Nat.radical_pos`, `Nat.radical_eq_prod_primeFactors`, `AddMonoid.exponent_pi`, `Function.minimalPeriod_piMap_fintype`, `Int.radical_natCast`, `Monoid.lcm_orderOf_eq_exponent`, `Monoid.lcm_orderOf_dvd_exponent`, `Equiv.Perm.lcm_cycleType`, `Nat.radical_le_self_iff`, `Finset.lcm_eq_prod`, `Pi.orderOf`, `ArithmeticFunction.carmichael_finset_lcm`, `ArithmeticFunction.carmichael_finset_prod`, `UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors`, `AddMonoid.lcm_addOrderOf_eq_exponent`, `Nat.self_lt_radical_iff`, `Nat.one_lt_radical_iff`, `ArithmeticFunction.carmichael_factorization`, `Int.radical_natAbs_eq_radical`, `Nat.radical_eq_one_iff`, `AddMonoid.lcm_addOrderOf_dvd_exponent`, `Nat.radical_le_one_iff`

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