Option

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

Statistics

Metric	Count
Definitions `optionElim`, `optionEquiv`, `some`	3
Theorems `embDomain_some_none`, `embDomain_some_some`, `eq_option_embedding_update_none_iff`, `optionElim_apply_eq_elim`, `optionElim_apply_none`, `optionElim_apply_some`, `optionElim_eq_elim'`, `optionElim_ne_zero_iff`, `optionElim_ne_zero_of_left`, `optionElim_ne_zero_of_right`, `optionElim_some`, `optionElim_zero`, `optionEquiv_apply`, `optionEquiv_symm_apply`, `prod_option_index`, `some_add`, `some_apply`, `some_embDomain_some`, `some_optionElim`, `some_single_none`, `some_single_some`, `some_update_none`, `some_zero`, `sum_option_index`, `sum_option_index_smul`	25
Total	28

Finsupp

Definitions

Name	Category	Theorems
`optionElim` 📖	CompOp	9 math math: `optionElim_some`, `optionElim_eq_elim'`, `MvPolynomial.optionEquivLeft_coeff_coeff`, `MvPolynomial.mem_support_coeff_optionEquivLeft`, `optionElim_zero`, `optionElim_apply_some`, `optionElim_apply_eq_elim`, `some_optionElim`, `optionElim_apply_none`
`optionEquiv` 📖	CompOp	2 math math: `optionEquiv_symm_apply`, `optionEquiv_apply`
`some` 📖	CompOp	17 math math: `some_zero`, `some_embDomain_some`, `eq_option_embedding_update_none_iff`, `optionElim_some`, `some_add`, `MvPolynomial.optionEquivLeft_coeff_some_coeff_none`, `some_single_none`, `prod_option_index`, `sum_option_index_smul`, `some_update_none`, `linearCombination_option`, `MvPolynomial.optionEquivLeft_monomial`, `some_optionElim`, `some_single_some`, `optionEquiv_apply`, `some_apply`, `sum_option_index`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embDomain_some_none` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `embDomain` `Function.Embedding.some`	—	`embDomain_notin_range`
`embDomain_some_some` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `embDomain` `Function.Embedding.some`	—	`embDomain_apply_self`
`eq_option_embedding_update_none_iff` 📖	mathematical	—	`update` `embDomain` `Function.Embedding.some` `DFunLike.coe` `Finsupp` `instFunLike` `some`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`optionElim_apply_eq_elim` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `optionElim`	—	`optionElim_apply_none` `optionElim_apply_some`
`optionElim_apply_none` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `optionElim`	—	`coe_update` `Function.update_self`
`optionElim_apply_some` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `optionElim`	—	`coe_update` `Function.update_of_ne` `embDomain_some_some`
`optionElim_eq_elim'` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `optionElim` `Option.elim'`	—	`optionElim_apply_eq_elim` `Option.elim'_eq_elim`
`optionElim_ne_zero_iff` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `optionElim_zero` `single_zero` `optionElim_ne_zero_of_right` `optionElim_ne_zero_of_left`
`optionElim_ne_zero_of_left` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `optionElim_apply_eq_elim`
`optionElim_ne_zero_of_right` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `ext` `optionElim_apply_eq_elim`
`optionElim_some` 📖	mathematical	—	`optionElim` `DFunLike.coe` `Finsupp` `instFunLike` `some`	—	`ext` `optionElim_apply_none` `optionElim_apply_eq_elim`
`optionElim_zero` 📖	mathematical	—	`optionElim` `Finsupp` `instZero` `single`	—	`ext` `optionElim_apply_eq_elim` `single_eq_same` `single_eq_of_ne`
`optionEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `optionEquiv` `instFunLike` `some`	—	—
`optionEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `optionEquiv` `update` `embDomain` `Function.Embedding.some`	—	—
`prod_option_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddZero.toAdd` `MulOne.toMul`	`prod` `DFunLike.coe` `Finsupp` `instFunLike` `some`	—	`induction_linear` `some_zero` `mul_one` `prod_add_index` `some_add` `mul_mul_mul_comm` `prod_single_index` `single_eq_same` `some_single_none` `single_eq_of_ne` `some_single_some` `one_mul`
`some_add` 📖	mathematical	—	`some` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd`	—	`ext`
`some_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `some`	—	—
`some_embDomain_some` 📖	mathematical	—	`some` `embDomain` `Function.Embedding.some`	—	`ext` `some_apply` `embDomain_apply_self`
`some_optionElim` 📖	mathematical	—	`some` `optionElim`	—	`ext` `optionElim_apply_eq_elim`
`some_single_none` 📖	mathematical	—	`some` `single` `Finsupp` `instZero`	—	`ext` `single_eq_of_ne`
`some_single_some` 📖	mathematical	—	`some` `single`	—	`ext` `single_apply`
`some_update_none` 📖	mathematical	—	`some` `update`	—	`ext` `Function.update_of_ne`
`some_zero` 📖	mathematical	—	`some` `Finsupp` `instZero`	—	`ext`
`sum_option_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	`sum` `DFunLike.coe` `Finsupp` `instFunLike` `some`	—	`induction_linear` `some_zero` `add_zero` `sum_add_index` `Finset.mem_union` `mem_support_iff` `some_add` `add_add_add_comm` `sum_single_index` `single_eq_same` `some_single_none` `single_eq_of_ne` `some_single_some` `zero_add`
`sum_option_index_smul` 📖	mathematical	—	`sum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe` `Finsupp` `instFunLike` `some`	—	`sum_option_index` `zero_smul` `add_smul`

---

← Back to Index