WithTop

📁 Source: Mathlib/Algebra/BigOperators/WithTop.lean

Statistics

Metric	Count
Definitions	0
Theorems bot_lt_prod, bot_lt_sum_iff, coe_sum, prod_ne_bot, sum_eq_bot_iff, sum_lt_bot, coe_sum, prod_eq_top, prod_eq_top_ex_top, prod_eq_top_iff, prod_eq_top_ne_zero, prod_lt_top, prod_ne_top, sum_eq_top, sum_lt_top, sum_ne_top	16
Total	16

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_prod 📖	mathematical	WithBot instLT Bot.bot bot	Finset.prod CommMonoidWithZero.toCommMonoid instCommMonoidWithZero	—	Finset.prod_induction bot_lt_mul bot_lt_coe
bot_lt_sum_iff 📖	mathematical	—	WithBot instLT Bot.bot bot Finset.sum addCommMonoid	—	—
coe_sum 📖	mathematical	—	some Finset.sum WithBot addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
prod_ne_bot 📖	—	—	—	—	Finset.prod_induction mul_ne_bot coe_ne_bot
sum_eq_bot_iff 📖	mathematical	—	Finset.sum WithBot addCommMonoid Bot.bot bot Finset Finset.instMembership	—	Finset.cons_induction Finset.sum_cons
sum_lt_bot 📖	mathematical	—	WithBot instLT Bot.bot bot Finset.sum addCommMonoid	—	bot_lt_sum_iff bot_lt_iff_ne_bot

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_sum 📖	mathematical	—	some Finset.sum WithTop addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
prod_eq_top 📖	mathematical	Finset Finset.instMembership Top.top WithTop top	Finset.prod CommMonoidWithZero.toCommMonoid instCommMonoidWithZero	—	Finset.prod_erase_mul mul_eq_top_iff Finset.prod_ne_zero_iff nontrivial Nontrivial.to_nonempty instNoZeroDivisors
prod_eq_top_ex_top 📖	mathematical	Finset.prod WithTop CommMonoidWithZero.toCommMonoid instCommMonoidWithZero Top.top top	Finset Finset.instMembership	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq prod_ne_top
prod_eq_top_iff 📖	mathematical	—	Finset.prod WithTop CommMonoidWithZero.toCommMonoid instCommMonoidWithZero Top.top top Finset Finset.instMembership	—	prod_eq_top_ex_top prod_eq_top_ne_zero prod_eq_top
prod_eq_top_ne_zero 📖	—	Finset Finset.instMembership Finset.prod WithTop CommMonoidWithZero.toCommMonoid instCommMonoidWithZero Top.top top	—	—	top_ne_zero Finset.prod_eq_zero
prod_lt_top 📖	mathematical	WithTop instLT Top.top top	Finset.prod CommMonoidWithZero.toCommMonoid instCommMonoidWithZero	—	Finset.prod_induction mul_lt_top coe_lt_top
prod_ne_top 📖	—	—	—	—	Finset.prod_induction mul_ne_top coe_ne_top
sum_eq_top 📖	mathematical	—	Finset.sum WithTop addCommMonoid Top.top top Finset Finset.instMembership	—	Finset.cons_induction Finset.sum_cons
sum_lt_top 📖	mathematical	—	WithTop instLT Finset.sum addCommMonoid Top.top top	—	—
sum_ne_top 📖	—	—	—	—	—

---

← Back to Index