Fin

📁 Source: Mathlib/Data/Finsupp/Fin.lean

Statistics

Metric	Count
Definitions cons, tail	2
Theorems cons_ne_zero_iff, cons_ne_zero_of_left, cons_ne_zero_of_right, cons_right_injective, cons_succ, cons_support, cons_tail, cons_zero, cons_zero_zero, tail_apply, tail_cons, tail_update_succ, tail_update_zero	13
Total	15

Finsupp

Definitions

Name	Category	Theorems
cons 📖	CompOp	14 math math: MvPolynomial.mem_image_support_coeff_finSuccEquiv, cons_succ, MvPolynomial.finSuccEquiv_coeff_coeff, sum_cons, sum_cons', MvPolynomial.support_coeff_finSuccEquiv, cons_tail, cons_right_injective, MvPolynomial.image_support_finSuccEquiv, cons_zero, cons_support, MvPolynomial.mem_support_coeff_finSuccEquiv, tail_cons, cons_zero_zero
tail 📖	CompOp	5 math math: cons_tail, tail_update_zero, tail_update_succ, tail_cons, tail_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_ne_zero_iff 📖	—	—	—	—	imp_iff_not_or cons_zero_zero cons_ne_zero_of_left cons_ne_zero_of_right
cons_ne_zero_of_left 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose₄ cons_zero coe_zero Pi.zero_apply
cons_ne_zero_of_right 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose₄ ext
cons_right_injective 📖	mathematical	—	Finsupp cons	—	Equiv.injective Fin.cons_right_injective DFunLike.coe_injective
cons_succ 📖	mathematical	—	DFunLike.coe Finsupp instFunLike cons	—	—
cons_support 📖	mathematical	—	Finset Finset.instHasSubset support cons Finset.instInsert Finset.map Fin.succEmb	—	—
cons_tail 📖	mathematical	—	cons DFunLike.coe Finsupp instFunLike tail	—	ext cons_zero cons_succ tail_apply
cons_zero 📖	mathematical	—	DFunLike.coe Finsupp instFunLike cons	—	—
cons_zero_zero 📖	mathematical	—	cons Finsupp instZero	—	ext cons_succ
tail_apply 📖	mathematical	—	DFunLike.coe Finsupp instFunLike tail	—	—
tail_cons 📖	mathematical	—	tail cons	—	ext
tail_update_succ 📖	mathematical	—	tail update	—	ext coe_update Fin.tail_update_succ
tail_update_zero 📖	mathematical	—	tail update	—	coe_update Fin.tail_update_zero

---

← Back to Index