Theorems · Theorem · number theory
Nat.Ico_filter_coprime_le
∀ {a : ℕ} (k n : ℕ), a ≠ 0 → {x ∈ Finset.Ico k (k + n) | a.Coprime x}.card ≤ a.totient * (n / a + 1)- Defined in
- Mathlib.Data.Nat.Totient
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- mul_oneproof · cited by 3,885
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- Finset.cardstatement and proof · cited by 2,327
- MulZeroClass.mul_zeroproof · cited by 2,091
- le_reflproof · cited by 2,061
- le_of_ltproof · cited by 1,175
- Finset.filterstatement and proof · cited by 949
- add_le_addproof · cited by 666
- le_imp_le_of_le_of_leproof · cited by 576
- Finset.Icostatement and proof · cited by 450
Cited by1
Results whose statement or proof uses this declaration.
- Nat.primeCounting'_add_leproof · cited by 1