Support

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

Statistics

Metric	Count
Definitions	0
Theorems mem_span_support, support_mul, support_mul_single, support_mul_single_eq_image, support_mul_single_subset, support_neg, support_one, support_one_subset, support_single_mul, support_single_mul_eq_image, support_single_mul_subset, support_single_ne_zero, support_single_subset, support_sum	14
Total	14

SkewMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_span_support 📖	mathematical	—	SkewMonoidAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.image DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring MonoidHom.instFunLike of SetLike.coe Finset Finset.instSetLike support AddCommMonoid.toAddMonoid	—	Fintype.mem_span_image_iff_exists_fun Finset.sum_congr of_apply smul_single mul_one Finsupp.sum_attach_index sum_single
support_mul 📖	mathematical	—	Finset Finset.instHasSubset support AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SkewMonoidAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Finset.mul	—	HasSubset.Subset.trans Finset.instIsTransSubset support_sum Finset.biUnion_subset support_single_subset Finset.singleton_subset_iff Finset.mem_image₂_of_mem
support_mul_single 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	support AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SkewMonoidAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.map mulRightEmbedding	—	Finset.ext support_mul_single_eq_image IsRightRegular.all
support_mul_single_eq_image 📖	mathematical	IsRightRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	support AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SkewMonoidAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.image	—	subset_antisymm Finset.instAntisymmSubset support_mul_single_subset coeff_mul sum_single_index smul_zero MulZeroClass.mul_zero sum_ite_eq' mem_support_iff
support_mul_single_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SkewMonoidAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.image	—	HasSubset.Subset.trans Finset.instIsTransSubset support_mul Finset.image₂_subset_left support_single_subset Finset.image₂_singleton_right subset_refl Finset.instReflSubset
support_neg 📖	mathematical	—	support SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SkewMonoidAlgebra NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass instNeg AddCommGroup.toAddGroup	—	support.eq_1 toFinsupp_neg Finsupp.support_neg support_toFinsupp
support_one 📖	mathematical	—	support AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instOne Finset Finset.one	—	Finsupp.support_single_ne_zero one_ne_zero
support_one_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instOne Finset.one	—	Finsupp.support_single_subset
support_single_mul 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	support AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.map mulLeftEmbedding AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finset.ext support_single_mul_eq_image IsLeftRegular.all
support_single_mul_eq_image 📖	mathematical	IsLeftRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	support AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.image AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	subset_antisymm Finset.instAntisymmSubset support_single_mul_subset coeff_mul sum_single_index MulZeroClass.zero_mul sum_zero sum_ite_eq' mem_support_iff
support_single_mul_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction single Finset.image AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	HasSubset.Subset.trans Finset.instIsTransSubset support_mul Finset.image₂_subset_right support_single_subset Finset.image₂_singleton_left subset_refl Finset.instReflSubset
support_single_ne_zero 📖	mathematical	—	support AddCommMonoid.toAddMonoid single Finset Finset.instSingleton	—	Finsupp.support_single_ne_zero
support_single_subset 📖	mathematical	—	Finset Finset.instHasSubset support AddCommMonoid.toAddMonoid single Finset.instSingleton	—	Finsupp.support_single_subset
support_sum 📖	mathematical	—	Finset Finset.instHasSubset support AddCommMonoid.toAddMonoid sum SkewMonoidAlgebra AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddCommMonoid Finset.biUnion coeff	—	toFinsupp_sum' Finsupp.support_sum

---

← Back to Index