Documentation Verification Report

FactorisationProperties

📁 Source: Mathlib/NumberTheory/FactorisationProperties.lean

Statistics

Metric	Count
Definitions `Abundant`, `Deficient`, `Pseudoperfect`, `Weird`, `abundancyIndex`, `instDecidableAbundant`, `instDecidableDeficient`, `instDecidablePseudoperfect`, `instDecidableWeird`	9
Theorems `deficient`, `mul_left`, `of_dvd`, `pseudoperfect`, `deficient`, `deficient_pow`, `not_abundant`, `not_perfect`, `not_pseudoperfect`, `not_weird`, `abundancyIndex_le_of_dvd`, `abundant_iff_not_perfect_and_not_deficient`, `abundant_iff_sum_divisors`, `abundant_iff_two_lt_abundancyIndex`, `abundant_twelve`, `deficient_iff_not_abundant_and_not_perfect`, `deficient_one`, `deficient_or_perfect_or_abundant`, `deficient_three`, `deficient_two`, `infinite_deficient`, `infinite_even_abundant`, `infinite_even_deficient`, `infinite_odd_abundant`, `infinite_odd_deficient`, `not_abundant_zero`, `not_pseudoperfect_iff_forall`, `perfect_iff_not_abundant_and_not_deficient`, `weird_seventy`	29
Total	38

IsPrimePow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deficient` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero`	`Nat.Deficient`	—	`Nat.Prime.deficient_pow` `Prime.nat_prime`

Nat

Definitions

Name	Category	Theorems
`Abundant` 📖	MathDef	11 math math: `abundant_iff_not_perfect_and_not_deficient`, `not_abundant_zero`, `infinite_odd_abundant`, `infinite_even_abundant`, `abundant_iff_two_lt_abundancyIndex`, `Prime.not_abundant`, `deficient_or_perfect_or_abundant`, `deficient_iff_not_abundant_and_not_perfect`, `abundant_iff_sum_divisors`, `abundant_twelve`, `perfect_iff_not_abundant_and_not_deficient`
`Deficient` 📖	MathDef	13 math math: `abundant_iff_not_perfect_and_not_deficient`, `infinite_deficient`, `infinite_odd_deficient`, `deficient_three`, `deficient_one`, `infinite_even_deficient`, `deficient_or_perfect_or_abundant`, `deficient_iff_not_abundant_and_not_perfect`, `Prime.deficient_pow`, `Prime.deficient`, `perfect_iff_not_abundant_and_not_deficient`, `IsPrimePow.deficient`, `deficient_two`
`Pseudoperfect` 📖	MathDef	3 math math: `Perfect.pseudoperfect`, `not_pseudoperfect_iff_forall`, `Prime.not_pseudoperfect`
`Weird` 📖	MathDef	2 math math: `weird_seventy`, `Prime.not_weird`
`abundancyIndex` 📖	CompOp	2 math math: `abundant_iff_two_lt_abundancyIndex`, `abundancyIndex_le_of_dvd`
`instDecidableAbundant` 📖	CompOp	—
`instDecidableDeficient` 📖	CompOp	—
`instDecidablePseudoperfect` 📖	CompOp	—
`instDecidableWeird` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abundancyIndex_le_of_dvd` 📖	mathematical	—	`abundancyIndex`	—	`abundancyIndex.eq_1` `cast_mul` `div_mul_eq_div_div_swap` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `le_div_iff₀` `cast_le` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Rat.instCharZero` `Finset.sum_mul` `Eq.trans_le` `Finset.sum_image` `Function.Injective.injOn` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `instIsCancelMulZero` `Finset.sum_le_sum_of_subset` `instCanonicallyOrderedAdd` `cast_nonneg` `IsStrictOrderedRing.toIsOrderedRing`
`abundant_iff_not_perfect_and_not_deficient` 📖	mathematical	—	`Abundant` `Perfect` `Deficient`	—	—
`abundant_iff_sum_divisors` 📖	mathematical	—	`Abundant` `Finset.sum` `instAddCommMonoid` `divisors`	—	—
`abundant_iff_two_lt_abundancyIndex` 📖	mathematical	—	`Abundant` `abundancyIndex`	—	`Finset.sum_congr` `properDivisors_zero` `divisors_zero` `cast_zero` `div_zero` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `instAtLeastTwoHAddOfNat` `abundant_iff_sum_divisors` `abundancyIndex.eq_1` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `cast_pos'` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `lt_of_le_of_ne'` `zero_le` `instCanonicallyOrderedAdd`
`abundant_twelve` 📖	mathematical	—	`Abundant`	—	—
`deficient_iff_not_abundant_and_not_perfect` 📖	mathematical	—	`Deficient` `Abundant` `Perfect`	—	—
`deficient_one` 📖	mathematical	—	`Deficient`	—	—
`deficient_or_perfect_or_abundant` 📖	mathematical	—	`Deficient` `Abundant` `Perfect`	—	—
`deficient_three` 📖	mathematical	—	`Deficient`	—	—
`deficient_two` 📖	mathematical	—	`Deficient`	—	—
`infinite_deficient` 📖	mathematical	—	`Set.Infinite` `setOf` `Deficient`	—	`Set.infinite_iff_exists_gt` `exists_infinite_primes` `Prime.deficient`
`infinite_even_abundant` 📖	mathematical	—	`Set.Infinite` `setOf` `Even` `Abundant`	—	`Set.infinite_iff_exists_gt`
`infinite_even_deficient` 📖	mathematical	—	`Set.Infinite` `setOf` `Even` `Deficient`	—	`Set.infinite_iff_exists_gt` `pow_succ` `instAtLeastTwoHAddOfNat` `mul_two` `Prime.deficient_pow` `prime_two` `lt_add_one` `instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`infinite_odd_abundant` 📖	mathematical	—	`Set.Infinite` `setOf` `Odd` `instSemiring` `Abundant`	—	`Set.infinite_iff_exists_gt`
`infinite_odd_deficient` 📖	mathematical	—	`Set.Infinite` `setOf` `Odd` `instSemiring` `Deficient`	—	`Set.infinite_iff_exists_gt` `exists_infinite_primes` `Set.mem_setOf` `Prime.odd_of_ne_two` `Prime.deficient`
`not_abundant_zero` 📖	mathematical	—	`Abundant`	—	—
`not_pseudoperfect_iff_forall` 📖	mathematical	—	`Pseudoperfect`	—	—
`perfect_iff_not_abundant_and_not_deficient` 📖	mathematical	—	`Perfect` `Abundant` `Deficient`	—	—
`weird_seventy` 📖	mathematical	—	`Weird`	—	—

Nat.Abundant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_left` 📖	—	`Nat.Abundant`	—	—	`mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `of_dvd`
`of_dvd` 📖	—	`Nat.Abundant`	—	—	`Nat.abundancyIndex_le_of_dvd`

Nat.Perfect

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pseudoperfect` 📖	mathematical	`Nat.Perfect`	`Nat.Pseudoperfect`	—	—

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deficient` 📖	mathematical	`Nat.Prime`	`Nat.Deficient`	—	`deficient_pow` `pow_one`
`deficient_pow` 📖	mathematical	`Nat.Prime`	`Nat.Deficient` `Monoid.toNatPow` `Nat.instMonoid`	—	`pow_zero` `Nat.deficient_one` `subset_antisymm` `Finset.instAntisymmSubset` `Nat.dvd_prime_pow` `lt_of_le_of_ne` `lt_irrefl` `two_le` `Finset.sum_image` `pow_injective_of_not_isUnit` `Nat.instIsCancelMulZero` `Irreducible.not_isUnit` `ne_zero` `Nat.Deficient.eq_1` `Nat.geomSum_eq` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `pos`
`not_abundant` 📖	mathematical	`Nat.Prime`	`Nat.Abundant`	—	`LT.lt.ne'` `LT.lt.trans` `one_lt` `Nat.sum_properDivisors_eq_one_iff_prime`
`not_perfect` 📖	mathematical	`Nat.Prime`	`Nat.Perfect`	—	`not_pseudoperfect` `not_imp_not` `Nat.Perfect.pseudoperfect`
`not_pseudoperfect` 📖	mathematical	`Nat.Prime`	`Nat.Pseudoperfect`	—	`properDivisors` `Finset.sum_singleton`
`not_weird` 📖	mathematical	`Nat.Prime`	`Nat.Weird`	—	—

---

← Back to Index