Gaps

📁 Source: Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean

Statistics

Metric	Count
Definitions	0
Theorems prod_eq_prod_range_intervalGapsWithin, prod_intervalGapsWithin_eq_div_div_prod, prod_intervalGapsWithin_mul_prod_eq_div, sum_eq_sum_range_intervalGapsWithin, sum_intervalGapsWithin_add_sum_eq_sub, sum_intervalGapsWithin_eq_sub_sub_sum	6
Total	6

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_eq_prod_range_intervalGapsWithin 📖	mathematical	card	prod CommGroup.toCommMonoid range intervalGapsWithin	—	prod_bij intervalGapsWithin_mapsTo intervalGapsWithin_injOn mem_range intervalGapsWithin_surjOn
prod_intervalGapsWithin_eq_div_div_prod 📖	mathematical	card	prod CommGroup.toCommMonoid range DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup intervalGapsWithin	—	eq_div_iff_mul_eq' prod_intervalGapsWithin_mul_prod_eq_div
prod_intervalGapsWithin_mul_prod_eq_div 📖	mathematical	card	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup prod CommGroup.toCommMonoid range DivInvMonoid.toDiv intervalGapsWithin	—	prod_eq_prod_range_intervalGapsWithin mul_comm prod_range_succ mul_assoc prod_mul_distrib prod_congr div_mul_div_cancel prod_range_div intervalGapsWithin.congr_simp Fin.natCast_eq_last Fin.natCast_zero intervalGapsWithin_zero_fst intervalGapsWithin_last_snd div_mul_div_cancel'
sum_eq_sum_range_intervalGapsWithin 📖	mathematical	card	sum AddCommGroup.toAddCommMonoid range intervalGapsWithin	—	sum_bij intervalGapsWithin_mapsTo intervalGapsWithin_injOn mem_range intervalGapsWithin_surjOn
sum_intervalGapsWithin_add_sum_eq_sub 📖	mathematical	card	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup sum AddCommGroup.toAddCommMonoid range SubNegMonoid.toSub intervalGapsWithin	—	sum_eq_sum_range_intervalGapsWithin add_comm sum_range_succ add_assoc sum_add_distrib sum_congr sub_add_sub_cancel sum_range_sub intervalGapsWithin.congr_simp Fin.natCast_eq_last Fin.natCast_zero intervalGapsWithin_zero_fst intervalGapsWithin_last_snd sub_add_sub_cancel'
sum_intervalGapsWithin_eq_sub_sub_sum 📖	mathematical	card	sum AddCommGroup.toAddCommMonoid range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup intervalGapsWithin	—	eq_sub_iff_add_eq sum_intervalGapsWithin_add_sum_eq_sub

---

← Back to Index