Documentation Verification Report

AuxResults

📁 Source: PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_factors_of_mult`, `conv_lambda_sq_larger_sum`, `div_mult_of_dvd_squarefree`, `inv_antitoneOn_Icc`, `inv_antitoneOn_pos`, `inv_sub_antitoneOn_Icc`, `inv_sub_antitoneOn_gt`, `ite_sum_zero`, `log_add_one_le_sum_inv`, `log_le_sum_inv`, `moebius_inv_dvd_lower_bound`, `moebius_inv_dvd_lower_bound'`, `moebius_inv_dvd_lower_bound_real`, `multiplicative_zero_of_zero_dvd`, `sum_inv_le_log`, `sum_inv_le_log_real`, `sum_over_dvd_ite`, `sum_pow_cardDistinctFactors_div_self_le_log_pow`, `sum_pow_cardDistinctFactors_le_self_mul_log_pow`	19
Total	19

ArithmeticFunction.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_factors_of_mult` 📖	—	—	—	—	—

Aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conv_lambda_sq_larger_sum` 📖	—	—	—	—	`ite_sum_zero`
`div_mult_of_dvd_squarefree` 📖	—	—	—	—	—
`inv_antitoneOn_Icc` 📖	—	—	—	—	`inv_sub_antitoneOn_Icc`
`inv_antitoneOn_pos` 📖	—	—	—	—	`inv_sub_antitoneOn_gt`
`inv_sub_antitoneOn_Icc` 📖	—	—	—	—	`inv_sub_antitoneOn_gt`
`inv_sub_antitoneOn_gt` 📖	—	—	—	—	—
`ite_sum_zero` 📖	—	—	—	—	—
`log_add_one_le_sum_inv` 📖	—	—	—	—	`inv_antitoneOn_Icc`
`log_le_sum_inv` 📖	—	—	—	—	`log_add_one_le_sum_inv`
`moebius_inv_dvd_lower_bound` 📖	—	—	—	—	—
`moebius_inv_dvd_lower_bound'` 📖	—	—	—	—	`moebius_inv_dvd_lower_bound` `sum_over_dvd_ite`
`moebius_inv_dvd_lower_bound_real` 📖	—	—	—	—	`moebius_inv_dvd_lower_bound'`
`multiplicative_zero_of_zero_dvd` 📖	—	—	—	—	—
`sum_inv_le_log` 📖	—	—	—	—	`inv_sub_antitoneOn_Icc`
`sum_inv_le_log_real` 📖	—	—	—	—	`sum_inv_le_log`
`sum_over_dvd_ite` 📖	—	—	—	—	—
`sum_pow_cardDistinctFactors_div_self_le_log_pow` 📖	—	—	—	—	`sum_inv_le_log_real`
`sum_pow_cardDistinctFactors_le_self_mul_log_pow` 📖	—	—	—	—	`sum_pow_cardDistinctFactors_div_self_le_log_pow`

---

← Back to Index