BigOperators

📁 Source: Mathlib/Tactic/NormNum/BigOperators.lean

Statistics

Metric	Count
Definitions ProveEmptyOrConsResult, eq_trans, uncheckedCast, proveEmptyOrCons, ProveNilOrConsResult, eq_trans, uncheckedCast, proveNilOrCons, ProveZeroOrConsResult, eq_trans, uncheckedCast, proveZeroOrCons, UnifyZeroOrSuccResult, unifyZeroOrSucc, eq_trans, evalFinsetBigop, evalFinsetProd, evalFinsetSum	18
Theorems insert_eq_cons, range_succ', range_zero', univ_eq_elems, range_succ_eq_map', range_zero', insert_eq_cons, range_succ', range_zero', prod_empty, sum_empty	11
Total	29

Mathlib.Meta.Finset

Definitions

Name	Category	Theorems
ProveEmptyOrConsResult 📖	CompData	—
proveEmptyOrCons 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insert_eq_cons 📖	mathematical	Finset Finset.instMembership	Finset.instInsert Finset.cons	—	Finset.cons_eq_insert
range_succ' 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	Finset.range Finset.cons Finset.notMem_range_self	—	Finset.notMem_range_self Mathlib.Meta.NormNum.IsNat.out Nat.cast_id Finset.range_add_one insert_eq_cons
range_zero' 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	Finset.range Finset Finset.instEmptyCollection	—	Mathlib.Meta.NormNum.IsNat.out Nat.cast_zero Finset.range_zero
univ_eq_elems 📖	mathematical	Finset Finset.instMembership	Finset.univ	—	Finset.ext

Mathlib.Meta.Finset.ProveEmptyOrConsResult

Definitions

Name	Category	Theorems
eq_trans 📖	CompOp	—
uncheckedCast 📖	CompOp	—

Mathlib.Meta.List

Definitions

Name	Category	Theorems
ProveNilOrConsResult 📖	CompData	—
proveNilOrCons 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_succ_eq_map' 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	—	Mathlib.Meta.NormNum.IsNat.out Nat.cast_id
range_zero' 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	—	Mathlib.Meta.NormNum.IsNat.out Nat.cast_zero

Mathlib.Meta.List.ProveNilOrConsResult

Definitions

Name	Category	Theorems
eq_trans 📖	CompOp	—
uncheckedCast 📖	CompOp	—

Mathlib.Meta.Multiset

Definitions

Name	Category	Theorems
ProveZeroOrConsResult 📖	CompData	—
proveZeroOrCons 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insert_eq_cons 📖	mathematical	—	Multiset Multiset.instInsert Multiset.cons	—	—
range_succ' 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	Multiset.range Multiset.cons	—	Mathlib.Meta.NormNum.IsNat.out Nat.cast_id Multiset.range_succ
range_zero' 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	Multiset.range Multiset Multiset.instZero	—	Mathlib.Meta.NormNum.IsNat.out Nat.cast_zero Multiset.range_zero

Mathlib.Meta.Multiset.ProveZeroOrConsResult

Definitions

Name	Category	Theorems
eq_trans 📖	CompOp	—
uncheckedCast 📖	CompOp	—

Mathlib.Meta.Nat

Definitions

Name	Category	Theorems
UnifyZeroOrSuccResult 📖	CompData	—
unifyZeroOrSucc 📖	CompOp	—

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalFinsetBigop 📖	CompOp	—
evalFinsetProd 📖	CompOp	—
evalFinsetSum 📖	CompOp	—

Mathlib.Meta.NormNum.Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_empty 📖	mathematical	—	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid Finset Finset.instEmptyCollection	—	Nat.cast_one
sum_empty 📖	mathematical	—	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset Finset.instEmptyCollection	—	Nat.cast_zero

Mathlib.Meta.NormNum.Result

Definitions

Name	Category	Theorems
eq_trans 📖	CompOp	—

---

← Back to Index