MaricaSchoenheim

📁 Source: Mathlib/NumberTheory/MaricaSchoenheim.lean

Statistics

Metric	Count
Definitions GrahamConjecture	1
Theorems grahamConjecture_of_squarefree	1
Total	2

Nat

Definitions

Name	Category	Theorems
GrahamConjecture 📖	MathDef	1 math math: grahamConjecture_of_squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
grahamConjecture_of_squarefree 📖	mathematical	Squarefree instMonoid	GrahamConjecture	—	Squarefree.squarefree_of_dvd lt_irrefl Finset.card_image_of_injOn Finset.coe_Iio Set.InjOn.comp Set.LeftInvOn.injOn prod_primeFactors_invOn_squarefree StrictMonoOn.injOn card_Iio Finset.card_le_card_diffs Finset.card_le_card_of_injOn primeFactors_div_gcd Squarefree.ne_zero instNontrivial prod_primeFactors_of_squarefree Ne.bot_lt Mathlib.Tactic.Push.not_and_eq card_Ioo tsub_zero instOrderedSub tsub_lt_self instCanonicallyOrderedAdd IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_lt_one instZeroLEOneClass

---

← Back to Index