Documentation Verification Report

Support

📁 Source: Mathlib/Algebra/MonoidAlgebra/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems `mem_span_support`, `mem_span_support'`, `support_mul`, `support_mul_single`, `support_mul_single_eq_image`, `support_mul_single_subset`, `support_one`, `support_one_subset`, `support_single_mul`, `support_single_mul_eq_image`, `support_single_mul_subset`, `mem_span_support`, `support_mul`, `support_mul_single`, `support_mul_single_eq_image`, `support_mul_single_subset`, `support_one`, `support_one_subset`, `support_single_mul`, `support_single_mul_eq_image`, `support_single_mul_subset`	21
Total	21

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_span_support` 📖	mathematical	—	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `of'` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Set.image_congr` `Finsupp.supported_eq_span_single` `Finsupp.mem_supported` `subset_refl` `Set.instReflSubset`
`mem_span_support'` 📖	mathematical	—	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `of'` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mem_span_support`
`support_mul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul` `Finset.add`	—	`mul_def` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finsupp.support_sum` `Finset.biUnion_subset` `Finsupp.support_single_subset` `Finset.singleton_subset_iff` `Finset.mem_image₂_of_mem`
`support_mul_single` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finsupp.support` `AddMonoidAlgebra` `instMul` `single` `Finset.map` `addRightEmbedding`	—	`Finset.ext` `support_mul_single_eq_image` `IsAddRightRegular.all` `Finset.mem_image` `Finset.mem_map`
`support_mul_single_eq_image` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsAddRightRegular`	`Finsupp.support` `AddMonoidAlgebra` `instMul` `single` `Finset.image`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_mul_single_subset` `Finsupp.mem_support_iff` `mul_apply` `sum_single_index` `MulZeroClass.mul_zero` `Finsupp.sum_ite_eq'`
`support_mul_single_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul` `single` `Finset.image`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `support_mul` `Finset.image₂_subset_left` `Finsupp.support_single_subset` `Finset.image₂_singleton_right` `subset_refl` `Finset.instReflSubset`
`support_one` 📖	mathematical	—	`Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `zero` `Finset` `Finset.zero`	—	`Finsupp.support_single_ne_zero` `one_ne_zero`
`support_one_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `zero` `Finset.zero`	—	`Finsupp.support_single_subset`
`support_single_mul` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finsupp.support` `AddMonoidAlgebra` `instMul` `single` `Finset.map` `addLeftEmbedding`	—	`Finset.ext` `support_single_mul_eq_image` `IsAddLeftRegular.all` `Finset.mem_image` `Finset.mem_map`
`support_single_mul_eq_image` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsAddLeftRegular`	`Finsupp.support` `AddMonoidAlgebra` `instMul` `single` `Finset.image`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_single_mul_subset` `Finsupp.mem_support_iff` `mul_apply` `Finsupp.sum_single_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `Finsupp.sum_ite_eq'`
`support_single_mul_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul` `single` `Finset.image`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `support_mul` `Finset.image₂_subset_right` `Finsupp.support_single_subset` `Finset.image₂_singleton_left` `subset_refl` `Finset.instReflSubset`

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_span_support` 📖	mathematical	—	`MonoidAlgebra` `Submodule` `addCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Set.image_congr` `Finsupp.supported_eq_span_single` `Finsupp.mem_supported` `subset_refl` `Set.instReflSubset`
`support_mul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `instMul` `Finset.mul`	—	`mul_def` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finsupp.support_sum` `Finset.biUnion_subset` `Finsupp.support_single_subset` `Finset.singleton_subset_iff` `Finset.mem_image₂_of_mem`
`support_mul_single` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finsupp.support` `MonoidAlgebra` `instMul` `single` `Finset.map` `mulRightEmbedding`	—	`Finset.ext` `support_mul_single_eq_image` `IsRightRegular.all`
`support_mul_single_eq_image` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsRightRegular`	`Finsupp.support` `MonoidAlgebra` `instMul` `single` `Finset.image`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_mul_single_subset` `mul_apply` `sum_single_index` `MulZeroClass.mul_zero` `Finsupp.sum_ite_eq'` `Finsupp.mem_support_iff`
`support_mul_single_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `instMul` `single` `Finset.image`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `support_mul` `Finset.image₂_subset_left` `Finsupp.support_single_subset` `Finset.image₂_singleton_right` `subset_refl` `Finset.instReflSubset`
`support_one` 📖	mathematical	—	`Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `one` `Finset` `Finset.one`	—	`Finsupp.support_single_ne_zero` `one_ne_zero`
`support_one_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `one` `Finset.one`	—	`Finsupp.support_single_subset`
`support_single_mul` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finsupp.support` `MonoidAlgebra` `instMul` `single` `Finset.map` `mulLeftEmbedding`	—	`Finset.ext` `support_single_mul_eq_image` `IsLeftRegular.all`
`support_single_mul_eq_image` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsLeftRegular`	`Finsupp.support` `MonoidAlgebra` `instMul` `single` `Finset.image`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_single_mul_subset` `mul_apply` `Finsupp.sum_single_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `Finsupp.sum_ite_eq'` `Finsupp.mem_support_iff`
`support_single_mul_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `instMul` `single` `Finset.image`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `support_mul` `Finset.image₂_subset_right` `Finsupp.support_single_subset` `Finset.image₂_singleton_left` `subset_refl` `Finset.instReflSubset`

---

← Back to Index