Finset

📁 Source: Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean

Statistics

Metric	Count
Definitions distribMulAction, distribSMul, mulDistribMulAction, smulZeroClass	4
Theorems smul_zero, zero_smul, instNoZeroDivisors, inv_op_smul_finset_distrib₀, inv_smul_finset_distrib₀, inv_smul_mem_iff₀, mem_inv_smul_finset_iff₀, smul_finset_inter₀, smul_finset_neg, smul_finset_sdiff₀, smul_finset_subset_iff₀, smul_finset_subset_smul_finset_iff₀, smul_finset_symmDiff₀, smul_finset_univ₀, smul_mem_smul_finset_iff₀, smul_neg, smul_univ₀, smul_univ₀', smul_zero_subset, subset_smul_finset_iff₀, zero_mem_smul_finset, zero_smul_finset, zero_smul_finset_subset, zero_smul_subset	24
Total	28

Finset

Definitions

Name	Category	Theorems
distribMulAction 📖	CompOp	—
distribSMul 📖	CompOp	—
mulDistribMulAction 📖	CompOp	—
smulZeroClass 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors Finset mul zero	—	Function.Injective.noZeroDivisors coe_injective coe_zero coe_mul Set.instNoZeroDivisors
inv_op_smul_finset_distrib₀ 📖	mathematical	—	Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid MulOpposite smulFinset SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero SMulWithZero.toSMulZeroClass MulOpposite.instZero MulZeroClass.toOppositeSMulWithZero MulOpposite.op MulZeroClass.toSMulWithZero	—	eq_or_ne eq_empty_or_nonempty inv_zero zero_smul_finset inv_zero ext inv_inv mul_inv_rev
inv_smul_finset_distrib₀ 📖	mathematical	—	Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid smulFinset SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero MulOpposite MulOpposite.instZero MulZeroClass.toOppositeSMulWithZero MulOpposite.op	—	eq_or_ne eq_empty_or_nonempty inv_zero zero_smul_finset inv_zero ext inv_inv mul_inv_rev
inv_smul_mem_iff₀ 📖	mathematical	—	Finset instMembership SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid smulFinset	—	inv_smul_mem_iff
mem_inv_smul_finset_iff₀ 📖	mathematical	—	Finset instMembership smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	mem_inv_smul_finset_iff
smul_finset_inter₀ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction instInter	—	image_inter MulAction.injective₀
smul_finset_neg 📖	mathematical	—	Finset smulFinset SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	image_image smul_neg
smul_finset_sdiff₀ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction instSDiff	—	image_sdiff MulAction.injective₀
smul_finset_subset_iff₀ 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	smul_finset_subset_iff
smul_finset_subset_smul_finset_iff₀ 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	smul_finset_subset_smul_finset_iff
smul_finset_symmDiff₀ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	image_symmDiff MulAction.injective₀
smul_finset_univ₀ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction univ	—	coe_injective coe_smul_finset coe_univ Set.smul_set_univ₀
smul_mem_smul_finset_iff₀ 📖	mathematical	—	Finset instMembership smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	smul_mem_smul_finset_iff
smul_neg 📖	mathematical	—	Finset smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	image_image₂_right_comm smul_neg
smul_univ₀ 📖	mathematical	Finset instHasSubset zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	smul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid MulAction.toSemigroupAction univ	—	coe_injective coe_smul coe_univ Set.smul_univ₀ coe_zero coe_subset
smul_univ₀' 📖	mathematical	Nontrivial	Finset smul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction univ	—	coe_injective coe_smul coe_univ Set.smul_univ₀'
smul_zero_subset 📖	mathematical	—	Finset instHasSubset smul SMulZeroClass.toSMul zero	—	smul_zero
subset_smul_finset_iff₀ 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	subset_smul_finset_iff
zero_mem_smul_finset 📖	mathematical	Finset instMembership	smulFinset SMulZeroClass.toSMul	—	mem_smul_finset smul_zero
zero_smul_finset 📖	mathematical	Nonempty	Finset smulFinset SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	coe_injective coe_smul_finset coe_zero Set.zero_smul_set
zero_smul_finset_subset 📖	mathematical	—	Finset instHasSubset smulFinset SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	image_subset_iff mem_zero zero_smul
zero_smul_subset 📖	mathematical	—	Finset instHasSubset smul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	zero_smul

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_zero 📖	mathematical	Finset.Nonempty	Finset Finset.smul SMulZeroClass.toSMul Finset.zero	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset Finset.smul_zero_subset smul_zero
zero_smul 📖	mathematical	Finset.Nonempty	Finset Finset.smul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Finset.zero	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset Finset.zero_smul_subset zero_smul

---

← Back to Index