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 SkewMonoidAlgebra instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass 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 SkewMonoidAlgebra instMul 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 SkewMonoidAlgebra instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass 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 SkewMonoidAlgebra instMul 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