Documentation Verification Report

Indicator

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

Statistics

Metric	Count
Definitions `indicator`	1
Theorems `eq_indicator_iff`, `eq_indicator_self_iff`, `indicator_apply`, `indicator_indicator`, `indicator_injective`, `indicator_of_mem`, `indicator_of_notMem`, `single_eq_indicator`, `support_indicator_subset`	9
Total	10

Finsupp

Definitions

Name	Category	Theorems
`indicator` 📖	CompOp	17 math math: `sum_indicator_index`, `sum_indicator_index_eq_sum_attach`, `single_eq_indicator`, `eq_indicator_iff`, `indicator_of_notMem`, `indicator_apply`, `prod_indicator_index_eq_prod_attach`, `MvPolynomial.coeff_prod_X_pow`, `prod_indicator_index`, `indicator_eq_sum_attach_single`, `eq_indicator_self_iff`, `indicator_eq_sum_single`, `MvPolynomial.prod_X_pow`, `indicator_of_mem`, `support_indicator_subset`, `indicator_injective`, `indicator_indicator`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_indicator_iff` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `indicator` `Set` `Set.instHasSubset` `Function.support` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.subset_def` `indicator_apply`
`eq_indicator_self_iff` 📖	mathematical	—	`indicator` `DFunLike.coe` `Finsupp` `instFunLike` `Finset` `Finset.instHasSubset` `support`	—	—
`indicator_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `indicator` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.decidableMem`	—	—
`indicator_indicator` 📖	mathematical	—	`indicator` `DFunLike.coe` `Finsupp` `instFunLike` `Finset` `Finset.instInter` `Finset.mem_of_mem_inter_left`	—	—
`indicator_injective` 📖	mathematical	—	`Finsupp` `indicator`	—	`indicator_of_mem` `DFunLike.congr_fun`
`indicator_of_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `Finsupp` `instFunLike` `indicator`	—	—
`indicator_of_notMem` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `Finsupp` `instFunLike` `indicator`	—	—
`single_eq_indicator` 📖	mathematical	—	`single` `indicator` `Finset` `Finset.instSingleton`	—	`ext` `single_apply` `indicator_apply`
`support_indicator_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `indicator`	—	`mem_support_iff` `Finset.mem_coe` `indicator_of_notMem`

---

← Back to Index