Set

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

Statistics

Metric	Count
Definitions distribMulActionSet, distribSMulSet, mulDistribMulActionSet, smulZeroClassSet	4
Theorems smul_zero, zero_smul, instNoZeroDivisors, inv_op_smul_set_distrib₀, inv_smul_set_distrib₀, mem_inv_smul_set_iff₀, mem_smul_set_iff_inv_smul_mem₀, preimage_smul_inv₀, preimage_smul₀, smul_mem_smul_set_iff₀, smul_set_inter₀, smul_set_pi₀, smul_set_pi₀', smul_set_sdiff₀, smul_set_subset_iff₀, smul_set_subset_smul_set_iff₀, smul_set_symmDiff₀, smul_set_univ₀, smul_univ₀, smul_univ₀', smul_zero_subset, subset_smul_set_iff₀, subsingleton_zero_smul_set, zero_mem_smul_set, zero_smul_set, zero_smul_set_subset, zero_smul_subset	27
Total	31

Set

Definitions

Name	Category	Theorems
distribMulActionSet 📖	CompOp	—
distribSMulSet 📖	CompOp	—
mulDistribMulActionSet 📖	CompOp	—
smulZeroClassSet 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors Set mul zero	—	zero_nonempty Nonempty.subset_zero_iff Nonempty.of_smul_right Nonempty.of_smul_left NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero Eq.subset instReflSubset mul_mem_mul
inv_op_smul_set_distrib₀ 📖	mathematical	—	Set inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid MulOpposite smulSet 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 smul_set_empty inv_zero zero_smul_set inv_zero ext inv_inv mul_inv_rev
inv_smul_set_distrib₀ 📖	mathematical	—	Set inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid smulSet 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 smul_set_empty inv_zero zero_smul_set inv_zero ext inv_inv mul_inv_rev
mem_inv_smul_set_iff₀ 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	mem_inv_smul_set_iff
mem_smul_set_iff_inv_smul_mem₀ 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	mem_smul_set_iff_inv_smul_mem
preimage_smul_inv₀ 📖	mathematical	—	preimage SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Set smulSet	—	preimage_smul
preimage_smul₀ 📖	mathematical	—	preimage SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set smulSet InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	preimage_smul
smul_mem_smul_set_iff₀ 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	smul_mem_smul_set_iff
smul_set_inter₀ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction instInter	—	smul_set_inter
smul_set_pi₀ 📖	mathematical	—	Set smulSet Pi.instSMul SemigroupAction.toSMul SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction MonoidWithZero.toMonoid pi	—	smul_set_pi_of_isUnit
smul_set_pi₀' 📖	mathematical	univ	Set smulSet Pi.instSMul SemigroupAction.toSMul SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction MonoidWithZero.toMonoid pi	—	smul_set_pi_of_isUnit smul_set_univ_pi
smul_set_sdiff₀ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction instSDiff	—	image_diff MulAction.injective₀
smul_set_subset_iff₀ 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	smul_set_subset_iff_subset_inv_smul_set
smul_set_subset_smul_set_iff₀ 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	smul_set_subset_smul_set_iff
smul_set_symmDiff₀ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instSDiff	—	image_symmDiff MulAction.injective₀
smul_set_univ₀ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction univ	—	image_univ_of_surjective MulAction.surjective₀
smul_univ₀ 📖	mathematical	Set instHasSubset zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	smul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid MulAction.toSemigroupAction univ	—	not_subset eq_univ_of_forall smul_inv_smul₀
smul_univ₀' 📖	mathematical	Nontrivial	Set smul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction univ	—	smul_univ₀ Nontrivial.not_subset_singleton
smul_zero_subset 📖	mathematical	—	Set instHasSubset smul SMulZeroClass.toSMul zero	—	smul_zero
subset_smul_set_iff₀ 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	subset_smul_set_iff
subsingleton_zero_smul_set 📖	mathematical	—	Subsingleton Set smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	Subsingleton.anti subsingleton_singleton zero_smul_set_subset
zero_mem_smul_set 📖	mathematical	Set instMembership	smulSet SMulZeroClass.toSMul	—	smul_zero
zero_smul_set 📖	mathematical	Nonempty	Set smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	image_congr zero_smul Nonempty.image_const
zero_smul_set_subset 📖	mathematical	—	Set instHasSubset smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	image_subset_iff zero_smul
zero_smul_subset 📖	mathematical	—	Set instHasSubset smul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass zero	—	zero_smul

Set.Nonempty

Theorems

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

---

← Back to Index