Finite

📁 Source: Mathlib/Algebra/Group/Action/Pointwise/Set/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems of_smul_set, of_vadd_set, smul_set, vadd_set, finite_smul_set, finite_vadd_set, infinite_smul_set, infinite_vadd_set	8
Total	8

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_smul_set 📖	mathematical	—	Finite Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	finite_image_iff Function.Injective.injOn MulAction.injective
finite_vadd_set 📖	mathematical	—	Finite HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	finite_image_iff Function.Injective.injOn AddAction.injective
infinite_smul_set 📖	mathematical	—	Infinite Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	infinite_image_iff Function.Injective.injOn MulAction.injective
infinite_vadd_set 📖	mathematical	—	Infinite HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	infinite_image_iff Function.Injective.injOn AddAction.injective

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_smul_set 📖	mathematical	—	Set.Finite	—	Set.finite_smul_set
of_vadd_set 📖	mathematical	—	Set.Finite	—	Set.finite_vadd_set

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_set 📖	mathematical	Set.Infinite	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Set.infinite_smul_set
vadd_set 📖	mathematical	Set.Infinite	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Set.infinite_vadd_set

---

← Back to Index