Orbit

📁 Source: Mathlib/GroupTheory/FreeGroup/Orbit.lean

Statistics

Metric	Count
Definitions instSMulElemStartsWith, startsWith	2
Theorems duplicate, disjoint_iff_ne, ne_one, smul_def, startsWith_mk_mul	5
Total	7

FreeGroup

Definitions

Name	Category	Theorems
instSMulElemStartsWith 📖	CompOp	2 math math: startsWith.smul_def, Orbit.duplicate
startsWith 📖	CompOp	4 math math: startsWith.Injective, startsWith.disjoint_iff_ne, startsWith.smul_def, Orbit.duplicate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
startsWith_mk_mul 📖	mathematical	FreeGroup Set Set.instMembership startsWith	instMul	—	toWord_mul reduce_toWord mul_one zero_add

FreeGroup.Orbit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
duplicate 📖	mathematical	—	setOf Set Set.instMembership MulAction.orbit Set.Elem FreeGroup FreeGroup.startsWith FreeGroup.instSMulElemStartsWith SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MulAction.toSemigroupAction FreeGroup.instInv Set.instUnion Set.iUnion Set.instSingletonSet	—	Set.ext FreeGroup.mk_toWord zero_add FreeGroup.startsWith.smul_def inv_smul_smul FreeGroup.isReduced_cons_cons FreeGroup.isReduced_toWord Set.mem_biUnion SemigroupAction.mul_smul FreeGroup.IsReduced.reduce_eq FreeGroup.startsWith_mk_mul Disjoint.notMem_of_mem_left FreeGroup.startsWith.disjoint_iff_ne

FreeGroup.startsWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_iff_ne 📖	mathematical	—	Disjoint Set FreeGroup CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice FreeGroup.startsWith	—	zero_add
ne_one 📖	—	FreeGroup Set Set.instMembership FreeGroup.startsWith	—	—	—
smul_def 📖	mathematical	—	Set.Elem FreeGroup FreeGroup.startsWith FreeGroup.instSMulElemStartsWith SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid FreeGroup.instGroup MulAction.toSemigroupAction Set Set.instMembership	—	—

---

← Back to Index