Documentation Verification Report

MobiusLemma

📁 Source: PrimeNumberTheoremAnd/MobiusLemma.lean

Statistics

Metric	Count
Definitions `M`, `Q`, `R`, `sum_sq_div_moebius`	4
Theorems `integral_M_sqrt_div`, `mobius_lemma_1`, `mobius_lemma_1_sub`, `mobius_lemma_2`, `mobius_lemma_2_sub_1`, `mobius_lemma_2_sub_2`, `sq_dvd_mul_iff_of_coprime`, `sum_moebius_div_sq`, `sum_sq_div_moebius_eq_squarefree`, `sum_sq_div_moebius_is_multiplicative_explicit`, `sum_sq_div_moebius_prime_pow`	11
Total	15

MobiusLemma

Definitions

Name	Category	Theorems
`M` 📖	CompOp	5 math math: `mobius_lemma_2`, `mobius_lemma_1`, `integral_M_sqrt_div`, `mobius_lemma_2_sub_1`, `mobius_lemma_1_sub`
`Q` 📖	CompOp	1 math math: `mobius_lemma_1_sub`
`R` 📖	CompOp	2 math math: `mobius_lemma_2`, `mobius_lemma_1`
`sum_sq_div_moebius` 📖	CompOp	3 math math: `sum_sq_div_moebius_is_multiplicative_explicit`, `sum_sq_div_moebius_prime_pow`, `sum_sq_div_moebius_eq_squarefree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_M_sqrt_div` 📖	mathematical	—	`M`	—	—
`mobius_lemma_1` 📖	mathematical	—	`R` `M`	—	`mobius_lemma_1_sub` `integral_M_sqrt_div` `sum_moebius_div_sq`
`mobius_lemma_1_sub` 📖	mathematical	—	`Q` `M`	—	`sum_sq_div_moebius_eq_squarefree`
`mobius_lemma_2` 📖	mathematical	—	`R` `M`	—	`M.eq_1` `mobius_lemma_1` `mobius_lemma_2_sub_2` `mobius_lemma_2_sub_1`
`mobius_lemma_2_sub_1` 📖	mathematical	—	`M`	—	—
`mobius_lemma_2_sub_2` 📖	—	—	—	—	—
`sq_dvd_mul_iff_of_coprime` 📖	—	—	—	—	—
`sum_moebius_div_sq` 📖	—	—	—	—	—
`sum_sq_div_moebius_eq_squarefree` 📖	mathematical	—	`sum_sq_div_moebius`	—	`sum_sq_div_moebius_prime_pow` `sum_sq_div_moebius_is_multiplicative_explicit`
`sum_sq_div_moebius_is_multiplicative_explicit` 📖	mathematical	—	`sum_sq_div_moebius`	—	—
`sum_sq_div_moebius_prime_pow` 📖	mathematical	—	`sum_sq_div_moebius`	—	—

---

← Back to Index