Schnirelmann

📁 Source: Mathlib/Combinatorics/Schnirelmann.lean

Statistics

Metric	Count
Definitions schnirelmannDensity	1
Theorems exists_of_schnirelmannDensity_eq_zero, le_schnirelmannDensity_iff, schnirelmannDensity_congr, schnirelmannDensity_congr', schnirelmannDensity_diff_singleton_zero, schnirelmannDensity_empty, schnirelmannDensity_eq_one_iff, schnirelmannDensity_eq_one_iff_of_zero_mem, schnirelmannDensity_eq_zero_of_one_notMem, schnirelmannDensity_finite, schnirelmannDensity_finset, schnirelmannDensity_insert_zero, schnirelmannDensity_le_div, schnirelmannDensity_le_iff_forall, schnirelmannDensity_le_of_le, schnirelmannDensity_le_of_notMem, schnirelmannDensity_le_of_subset, schnirelmannDensity_le_one, schnirelmannDensity_lt_iff, schnirelmannDensity_mul_le_card_filter, schnirelmannDensity_nonneg, schnirelmannDensity_setOf_Odd, schnirelmannDensity_setOf_even, schnirelmannDensity_setOf_mod_eq_one, schnirelmannDensity_setOf_modeq_one, schnirelmannDensity_setOf_prime, schnirelmannDensity_univ	27
Total	28

(root)

Definitions

Name	Category	Theorems
schnirelmannDensity 📖	CompOp	26 math math: schnirelmannDensity_diff_singleton_zero, schnirelmannDensity_le_one, schnirelmannDensity_le_iff_forall, le_schnirelmannDensity_iff, schnirelmannDensity_congr', schnirelmannDensity_setOf_prime, schnirelmannDensity_finite, schnirelmannDensity_congr, schnirelmannDensity_setOf_even, schnirelmannDensity_le_of_le, schnirelmannDensity_eq_one_iff, schnirelmannDensity_eq_zero_of_one_notMem, schnirelmannDensity_univ, schnirelmannDensity_le_div, schnirelmannDensity_le_of_subset, schnirelmannDensity_lt_iff, schnirelmannDensity_setOf_modeq_one, schnirelmannDensity_le_of_notMem, schnirelmannDensity_insert_zero, schnirelmannDensity_eq_one_iff_of_zero_mem, schnirelmannDensity_setOf_Odd, schnirelmannDensity_setOf_mod_eq_one, schnirelmannDensity_empty, schnirelmannDensity_mul_le_card_filter, schnirelmannDensity_finset, schnirelmannDensity_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_of_schnirelmannDensity_eq_zero 📖	mathematical	Real Real.instLT Real.instZero schnirelmannDensity	DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	—	Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le le_schnirelmannDensity_iff Mathlib.Tactic.Push.not_and_eq
le_schnirelmannDensity_iff 📖	mathematical	—	Real Real.instLE schnirelmannDensity DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	—	le_ciInf_iff nonempty_gt Nat.instNoMaxOrder div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
schnirelmannDensity_congr 📖	mathematical	—	schnirelmannDensity	—	schnirelmannDensity_congr'
schnirelmannDensity_congr' 📖	mathematical	Set Set.instMembership	schnirelmannDensity	—	schnirelmannDensity.eq_1 Finset.ext
schnirelmannDensity_diff_singleton_zero 📖	mathematical	—	schnirelmannDensity Set Set.instSDiff Set.instSingletonSet	—	schnirelmannDensity_congr'
schnirelmannDensity_empty 📖	mathematical	—	schnirelmannDensity Set Set.instEmptyCollection Set.decidableEmptyset Real Real.instZero	—	schnirelmannDensity_eq_zero_of_one_notMem
schnirelmannDensity_eq_one_iff 📖	mathematical	—	schnirelmannDensity Real Real.instOne Set Set.instHasSubset Compl.compl Set.instCompl Set.instSingletonSet	—	le_antisymm_iff schnirelmannDensity_le_one not_imp_not not_le LE.le.trans_lt schnirelmannDensity_le_of_notMem IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial Nat.instCanonicallyOrderedAdd le_ciInf nonempty_gt Nat.instNoMaxOrder one_le_div Nat.cast_pos Nat.cast_le Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Finset.filter_true_of_mem LT.lt.ne' Finset.mem_Ioc Nat.card_Ioc le_refl
schnirelmannDensity_eq_one_iff_of_zero_mem 📖	mathematical	Set Set.instMembership	schnirelmannDensity Real Real.instOne Set.univ	—	schnirelmannDensity_eq_one_iff Set.eq_univ_of_forall eq_or_ne Set.subset_univ
schnirelmannDensity_eq_zero_of_one_notMem 📖	mathematical	Set Set.instMembership	schnirelmannDensity Real Real.instZero	—	LE.le.antisymm LE.le.trans schnirelmannDensity_le_of_notMem Nat.cast_one inv_one sub_self schnirelmannDensity_nonneg
schnirelmannDensity_finite 📖	mathematical	—	schnirelmannDensity Real Real.instZero	—	schnirelmannDensity.congr_simp Set.Finite.coe_toFinset schnirelmannDensity_finset
schnirelmannDensity_finset 📖	mathematical	—	schnirelmannDensity SetLike.coe Finset Finset.instSetLike Finset.decidableMem' Real Real.instZero	—	le_antisymm zero_add Real.instIsStrictOrderedRing div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_add_one LT.lt.trans_le' Nat.lt_floor_add_one div_le_div_of_nonneg_right Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Finset.card_le_card Finset.filter.congr_simp le_of_lt zero_lt_one NeZero.charZero_one IsStrictOrderedRing.toCharZero le_rfl LT.lt.trans_le le_of_not_ge schnirelmannDensity_nonneg
schnirelmannDensity_insert_zero 📖	mathematical	—	schnirelmannDensity Set Set.instInsert	—	schnirelmannDensity_congr'
schnirelmannDensity_le_div 📖	mathematical	—	Real Real.instLE schnirelmannDensity DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	—	ciInf_le div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Ne.bot_lt
schnirelmannDensity_le_iff_forall 📖	mathematical	—	Real Real.instLE schnirelmannDensity Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder Real.instAdd	—	le_iff_forall_pos_lt_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
schnirelmannDensity_le_of_le 📖	mathematical	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	schnirelmannDensity	—	LE.le.trans schnirelmannDensity_le_div
schnirelmannDensity_le_of_notMem 📖	mathematical	Set Set.instMembership	Real Real.instLE schnirelmannDensity Real.instSub Real.instOne Real.instInv Real.instNatCast	—	Nat.cast_zero inv_zero sub_zero schnirelmannDensity_le_one schnirelmannDensity_le_of_le LT.lt.ne' one_div one_sub_div Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_pred Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Finset.Ioo_insert_right Finset.filter_insert Finset.filter_subset LE.le.trans_eq Finset.card_le_card Nat.card_Ioo tsub_zero Nat.instOrderedSub le_of_lt Nat.cast_pos' NeZero.charZero_one
schnirelmannDensity_le_of_subset 📖	mathematical	Set Set.instHasSubset	Real Real.instLE schnirelmannDensity	—	ciInf_mono div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.mono_cast Finset.card_le_card Finset.monotone_filter_right Set.mem_of_subset_of_mem
schnirelmannDensity_le_one 📖	mathematical	—	Real Real.instLE schnirelmannDensity Real.instOne	—	schnirelmannDensity_le_of_le one_ne_zero Nat.cast_one div_one Nat.cast_le_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.card_filter_le
schnirelmannDensity_lt_iff 📖	mathematical	—	Real Real.instLT schnirelmannDensity DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	—	not_le le_schnirelmannDensity_iff
schnirelmannDensity_mul_le_card_filter 📖	mathematical	—	Real Real.instLE Real.instMul schnirelmannDensity Real.instNatCast Finset.card Finset.filter Set Set.instMembership Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder	—	eq_or_ne Nat.cast_zero MulZeroClass.mul_zero Finset.filter.congr_simp Finset.Ioc_eq_empty_of_le Finset.filter_empty le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd schnirelmannDensity_le_div
schnirelmannDensity_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero schnirelmannDensity	—	Real.iInf_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
schnirelmannDensity_setOf_Odd 📖	mathematical	—	schnirelmannDensity setOf Odd Nat.instSemiring Set.decidableSetOf Nat.instDecidablePredOdd Real Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Set.ext Nat.odd_iff Nat.instAtLeastTwoHAddOfNat schnirelmannDensity.congr_simp schnirelmannDensity_setOf_mod_eq_one Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_two
schnirelmannDensity_setOf_even 📖	mathematical	—	schnirelmannDensity setOf Even Set.decidableSetOf Nat.instDecidablePredEven Real Real.instZero	—	schnirelmannDensity_eq_zero_of_one_notMem
schnirelmannDensity_setOf_mod_eq_one 📖	mathematical	—	schnirelmannDensity setOf Set.decidableSetOf Real Real.instInv Real.instNatCast	—	Nat.cast_zero inv_zero schnirelmannDensity_finite le_antisymm schnirelmannDensity_le_of_le LT.lt.ne' one_div Nat.cast_one div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass eq_or_lt_of_le le_of_lt Nat.cast_pos' NeZero.charZero_one IsStrictOrderedRing.toCharZero le_schnirelmannDensity_iff Ne.lt_of_le' Nat.instCanonicallyOrderedAdd Nat.instZeroLEOneClass le_div_iff₀ Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial mul_comm div_eq_mul_inv LE.le.trans' Nat.cast_le Finset.card_le_card Finset.card_image_of_injective IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero Nat.card_Icc div_le_iff₀ Nat.cast_mul add_one_mul Distrib.rightDistribClass
schnirelmannDensity_setOf_modeq_one 📖	mathematical	—	schnirelmannDensity setOf Nat.ModEq Set.decidableSetOf Nat.instDecidableModEq Real Real.instInv Real.instNatCast	—	eq_or_ne schnirelmannDensity.congr_simp schnirelmannDensity_univ Nat.cast_one inv_one schnirelmannDensity_setOf_mod_eq_one
schnirelmannDensity_setOf_prime 📖	mathematical	—	schnirelmannDensity setOf Nat.Prime Set.decidableSetOf Nat.decidablePrime Real Real.instZero	—	schnirelmannDensity_eq_zero_of_one_notMem
schnirelmannDensity_univ 📖	mathematical	—	schnirelmannDensity Set.univ Set.decidableUniv Real Real.instOne	—	schnirelmannDensity_eq_one_iff_of_zero_mem

---

← Back to Index