Documentation Verification Report

Primorial

📁 Source: Mathlib/NumberTheory/Primorial.lean

Statistics

Metric	Count
Definitions `primorial`	1
Theorems `primorial_add`, `primorial_add_dvd`, `primorial_add_le`, `primorial_le_4_pow`, `primorial_pos`, `primorial_succ`	6
Total	7

(root)

Definitions

Name	Category	Theorems
`primorial` 📖	CompOp	7 math math: `primorial_succ`, `primorial_add`, `primorial_pos`, `primorial_add_dvd`, `Chebyshev.theta_eq_log_primorial`, `primorial_add_le`, `primorial_le_4_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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_le_4_pow` 📖	mathematical	—	`primorial` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.strong_induction_on` `le_refl` `Nat.even_or_odd` `add_right_comm` `primorial_add_le` `Nat.choose_symm_add` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `lt_add_iff_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.choose_middle_le_pow` `pow_add` `Decidable.eq_or_ne` `primorial_succ` `four_pos` `Nat.instZeroLEOneClass`
`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`

---

← Back to Index