Support

📁 Source: Mathlib/GroupTheory/GroupAction/Support.lean

Statistics

Metric	Count
Definitions Supports, Supports	2
Theorems mono, vadd, supports_of_mem, mono, smul, supports_of_mem	6
Total	8

AddAction

Definitions

Name	Category	Theorems
Supports 📖	MathDef	1 math math: supports_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
supports_of_mem 📖	mathematical	Set Set.instMembership	Supports	—	—

AddAction.Supports

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Set Set.instHasSubset AddAction.Supports	—	—	—
vadd 📖	mathematical	AddAction.Supports	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	VAddCommClass.vadd_comm Set.forall_mem_image vadd_left_cancel_iff

MulAction

Definitions

Name	Category	Theorems
Supports 📖	MathDef	1 math math: supports_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
supports_of_mem 📖	mathematical	Set Set.instMembership	Supports	—	—

MulAction.Supports

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Set Set.instHasSubset MulAction.Supports	—	—	—
smul 📖	mathematical	MulAction.Supports	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	SMulCommClass.smul_comm Set.forall_mem_image smul_left_cancel_iff

---

← Back to Index