Documentation Verification Report

Primorial

📁 Source: Mathlib/NumberTheory/Primorial.lean

Statistics

Metric	Count
Definitions `primorial`	1
Theorems `dvd_primorial`, `dvd_primorial_iff`, `dvd_primorial`, `le_primorial_self`, `lt_primorial_self`, `primorial_add`, `primorial_add_dvd`, `primorial_add_le`, `primorial_dvd_primorial`, `primorial_le_4_pow`, `primorial_le_four_pow`, `primorial_lt_four_pow`, `primorial_mono`, `primorial_monotone`, `primorial_one`, `primorial_pos`, `primorial_succ`, `primorial_two`, `primorial_zero`	19
Total	20

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_primorial` 📖	mathematical	`Nat.Prime`	`primorial`	—	`dvd_primorial_iff` `le_rfl`
`dvd_primorial_iff` 📖	mathematical	`Nat.Prime`	`primorial`	—	`Prime.dvd_finset_prod_iff` `prime` `LE.le.trans` `pos` `Finset.dvd_prod_of_mem`

Squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_primorial` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`primorial`	—	`Finset.prod_dvd_prod_of_subset` `Nat.prod_primeFactors_of_squarefree`

(root)

Definitions

Name	Category	Theorems
`primorial` 📖	CompOp	20 math math: `le_primorial_self`, `primorial_succ`, `primorial_le_four_pow`, `primorial_add`, `primorial_lt_four_pow`, `primorial_monotone`, `primorial_pos`, `lt_primorial_self`, `primorial_add_dvd`, `Squarefree.dvd_primorial`, `Chebyshev.theta_eq_log_primorial`, `primorial_add_le`, `Nat.Prime.dvd_primorial`, `primorial_le_4_pow`, `primorial_mono`, `primorial_dvd_primorial`, `primorial_two`, `primorial_one`, `Nat.Prime.dvd_primorial_iff`, `primorial_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_primorial_self` 📖	mathematical	—	`primorial`	—	`le_or_gt` `LT.lt.le` `lt_primorial_self`
`lt_primorial_self` 📖	mathematical	—	`primorial`	—	`Finset.single_le_prod'` `Nat.instMulLeftMono` `Nat.Prime.dvd_primorial_iff` `Nat.minFac_prime`
`primorial_add` 📖	mathematical	—	`primorial` `Finset.prod` `Nat.instCommMonoid` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`primorial.eq_1` `Nat.Ico_zero_eq_range` `Finset.prod_union` `Finset.disjoint_filter_filter` `Finset.Ico_disjoint_Ico_consecutive` `Finset.filter_union` `Finset.Ico_union_Ico_eq_Ico`
`primorial_add_dvd` 📖	mathematical	—	`primorial` `Nat.choose`	—	`primorial_add` `mul_dvd_mul_left` `Finset.prod_primes_dvd` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.Prime.prime` `Finset.mem_filter` `Nat.Prime.dvd_choose_add` `Finset.mem_Ico` `LE.le.trans_lt` `LT.lt.trans_le`
`primorial_add_le` 📖	mathematical	—	`primorial` `Nat.choose`	—	`mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `primorial_pos` `Nat.choose_pos` `primorial_add_dvd`
`primorial_dvd_primorial` 📖	mathematical	—	`primorial`	—	`Finset.prod_dvd_prod_of_subset` `Finset.filter_subset_filter` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`primorial_le_4_pow` 📖	mathematical	—	`primorial` `Monoid.toPow` `Nat.instMonoid`	—	`primorial_le_four_pow`
`primorial_le_four_pow` 📖	mathematical	—	`primorial` `Monoid.toPow` `Nat.instMonoid`	—	`eq_or_ne` `LT.lt.le` `primorial_lt_four_pow`
`primorial_lt_four_pow` 📖	mathematical	—	`primorial` `Monoid.toPow` `Nat.instMonoid`	—	`Nat.strong_induction_on` `Nat.even_or_odd` `add_right_comm` `primorial_add_le` `Nat.choose_symm_add` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `Nat.choose_middle_le_pow` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `pow_add` `le_refl` `Decidable.eq_or_ne` `primorial_succ` `four_pos` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`primorial_mono` 📖	mathematical	—	`primorial`	—	`Finset.prod_le_prod_of_subset_of_one_le'` `Nat.instMulLeftMono` `Finset.filter_subset_filter` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`primorial_monotone` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `primorial`	—	`primorial_mono`
`primorial_one` 📖	mathematical	—	`primorial`	—	—
`primorial_pos` 📖	mathematical	—	`primorial`	—	`Finset.prod_pos` `Nat.instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instNontrivial` `Nat.Prime.pos` `Finset.mem_filter`
`primorial_succ` 📖	mathematical	`Odd` `Nat.instSemiring`	`primorial`	—	`Finset.prod_congr` `Finset.range_add_one` `Finset.filter_insert` `Nat.not_even_iff_odd` `Nat.Prime.even_sub_one`
`primorial_two` 📖	mathematical	—	`primorial`	—	—
`primorial_zero` 📖	mathematical	—	`primorial`	—	—

---

← Back to Index