CyclicallyReduced

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

Statistics

Metric	Count
Definitions IsCyclicallyReduced, reduceCyclically, conjugator, IsCyclicallyReduced, reduceCyclically, conjugator	6
Theorems flatten_replicate, isReduced, nil, singleton, append_flatten_replicate_append, instIsAddTorsionFree, isCyclicallyReduced_cons_append_iff, isCyclicallyReduced_iff, conj_conjugator_reduceCyclically, cons_append, nil, singleton, cons_append, isCyclicallyReduced, nil, reduce_flatten_replicate, reduce_flatten_replicate_succ, singleton, flatten_replicate, isReduced, nil, singleton, append_flatten_replicate_append, instIsMulTorsionFree, isCyclicallyReduced_cons_append_iff, isCyclicallyReduced_iff, conj_conjugator_reduceCyclically, cons_append, nil, singleton, cons_append, isCyclicallyReduced, nil, reduce_flatten_replicate, reduce_flatten_replicate_succ, singleton	36
Total	42

FreeAddGroup

Definitions

Name	Category	Theorems
IsCyclicallyReduced 📖	MathDef	5 math math: IsCyclicallyReduced.nil, reduceCyclically.isCyclicallyReduced, isCyclicallyReduced_iff, isCyclicallyReduced_cons_append_iff, IsCyclicallyReduced.singleton
reduceCyclically 📖	CompOp	7 math math: reduceCyclically.isCyclicallyReduced, reduceCyclically.cons_append, reduceCyclically.singleton, reduceCyclically.conj_conjugator_reduceCyclically, reduceCyclically.reduce_flatten_replicate, reduceCyclically.nil, reduceCyclically.reduce_flatten_replicate_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddTorsionFree 📖	mathematical	—	IsAddTorsionFree FreeAddGroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddGroup	—	mul_comm mul_nsmul toWord_nsmul reduceCyclically.reduce_flatten_replicate isReduced_toWord mul_eq_zero IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instAtLeastTwoHAddOfNat OfNat.ofNat_ne_zero Nat.instCharZero List.sum_replicate negRev_length mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero reduceCyclically.conj_conjugator_reduceCyclically mk_toWord
isCyclicallyReduced_cons_append_iff 📖	mathematical	—	IsCyclicallyReduced IsReduced	—	isCyclicallyReduced_iff
isCyclicallyReduced_iff 📖	mathematical	—	IsCyclicallyReduced IsReduced	—	—

FreeAddGroup.IsCyclicallyReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flatten_replicate 📖	—	FreeAddGroup.IsCyclicallyReduced	—	—	nil FreeAddGroup.isCyclicallyReduced_iff FreeAddGroup.IsReduced.eq_1 List.isChain_flatten one_ne_zero isReduced List.isChain_replicate_of_rel List.getLast?_flatten_replicate List.head?_flatten_replicate
isReduced 📖	mathematical	FreeAddGroup.IsCyclicallyReduced	FreeAddGroup.IsReduced	—	—
nil 📖	mathematical	—	FreeAddGroup.IsCyclicallyReduced	—	FreeAddGroup.IsReduced.nil IsEmpty.forall_iff instIsEmptyFalse
singleton 📖	mathematical	—	FreeAddGroup.IsCyclicallyReduced	—	FreeAddGroup.IsReduced.singleton

FreeAddGroup.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_flatten_replicate_append 📖	—	FreeAddGroup.IsCyclicallyReduced FreeAddGroup.IsReduced	—	—	one_ne_zero append_overlap infix FreeAddGroup.IsCyclicallyReduced.isReduced FreeAddGroup.IsCyclicallyReduced.flatten_replicate

FreeAddGroup.reduceCyclically

Definitions

Name	Category	Theorems
conjugator 📖	CompOp	6 math math: conjugator.singleton, conjugator.nil, conj_conjugator_reduceCyclically, conjugator.cons_append, reduce_flatten_replicate, reduce_flatten_replicate_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_conjugator_reduceCyclically 📖	mathematical	—	conjugator FreeAddGroup.reduceCyclically FreeAddGroup.negRev	—	conjugator.nil nil conjugator.singleton singleton cons_append conjugator.cons_append
cons_append 📖	mathematical	—	FreeAddGroup.reduceCyclically	—	List.bidirectionalRec_cons_append
isCyclicallyReduced 📖	mathematical	FreeAddGroup.IsReduced	FreeAddGroup.IsCyclicallyReduced FreeAddGroup.reduceCyclically	—	nil FreeAddGroup.IsCyclicallyReduced.nil singleton FreeAddGroup.IsCyclicallyReduced.singleton cons_append FreeAddGroup.isCyclicallyReduced_cons_append_iff FreeAddGroup.IsReduced.infix
nil 📖	mathematical	—	FreeAddGroup.reduceCyclically	—	List.bidirectionalRec_nil
reduce_flatten_replicate 📖	mathematical	FreeAddGroup.IsReduced	FreeAddGroup.reduce conjugator FreeAddGroup.reduceCyclically FreeAddGroup.negRev	—	reduce_flatten_replicate_succ
reduce_flatten_replicate_succ 📖	mathematical	FreeAddGroup.IsReduced	FreeAddGroup.reduce conjugator FreeAddGroup.reduceCyclically FreeAddGroup.negRev	—	zero_add conj_conjugator_reduceCyclically FreeAddGroup.isReduced_iff_reduce_eq FreeAddGroup.reduce_append_reduce_reduce FreeAddGroup.IsReduced.reduce_eq FreeAddGroup.reduce.sound neg_one_zsmul add_assoc Mathlib.Tactic.Group.zsmul_trick_zero' neg_add_cancel zero_zsmul add_zero FreeAddGroup.IsReduced.append_flatten_replicate_append one_ne_zero isCyclicallyReduced
singleton 📖	mathematical	—	FreeAddGroup.reduceCyclically	—	List.bidirectionalRec_singleton

FreeAddGroup.reduceCyclically.conjugator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_append 📖	mathematical	—	FreeAddGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_cons_append
nil 📖	mathematical	—	FreeAddGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_nil
singleton 📖	mathematical	—	FreeAddGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_singleton

FreeGroup

Definitions

Name	Category	Theorems
IsCyclicallyReduced 📖	MathDef	5 math math: isCyclicallyReduced_cons_append_iff, isCyclicallyReduced_iff, IsCyclicallyReduced.nil, IsCyclicallyReduced.singleton, reduceCyclically.isCyclicallyReduced
reduceCyclically 📖	CompOp	7 math math: reduceCyclically.reduce_flatten_replicate_succ, reduceCyclically.nil, reduceCyclically.conj_conjugator_reduceCyclically, reduceCyclically.isCyclicallyReduced, reduceCyclically.cons_append, reduceCyclically.reduce_flatten_replicate, reduceCyclically.singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree FreeGroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	mul_comm pow_mul toWord_pow reduceCyclically.reduce_flatten_replicate IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instCharZero Nat.instAtLeastTwoHAddOfNat List.sum_replicate invRev_length mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero reduceCyclically.conj_conjugator_reduceCyclically mk_toWord
isCyclicallyReduced_cons_append_iff 📖	mathematical	—	IsCyclicallyReduced IsReduced	—	isCyclicallyReduced_iff
isCyclicallyReduced_iff 📖	mathematical	—	IsCyclicallyReduced IsReduced	—	—

FreeGroup.IsCyclicallyReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flatten_replicate 📖	—	FreeGroup.IsCyclicallyReduced	—	—	FreeGroup.isCyclicallyReduced_iff FreeGroup.IsReduced.eq_1 List.isChain_flatten isReduced List.isChain_replicate_of_rel List.getLast?_flatten_replicate List.head?_flatten_replicate
isReduced 📖	mathematical	FreeGroup.IsCyclicallyReduced	FreeGroup.IsReduced	—	—
nil 📖	mathematical	—	FreeGroup.IsCyclicallyReduced	—	instIsEmptyFalse
singleton 📖	mathematical	—	FreeGroup.IsCyclicallyReduced	—	—

FreeGroup.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_flatten_replicate_append 📖	—	FreeGroup.IsCyclicallyReduced FreeGroup.IsReduced	—	—	append_overlap infix FreeGroup.IsCyclicallyReduced.isReduced FreeGroup.IsCyclicallyReduced.flatten_replicate

FreeGroup.reduceCyclically

Definitions

Name	Category	Theorems
conjugator 📖	CompOp	6 math math: reduce_flatten_replicate_succ, conjugator.cons_append, conj_conjugator_reduceCyclically, reduce_flatten_replicate, conjugator.nil, conjugator.singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_conjugator_reduceCyclically 📖	mathematical	—	conjugator FreeGroup.reduceCyclically FreeGroup.invRev	—	conjugator.nil nil conjugator.singleton singleton cons_append conjugator.cons_append
cons_append 📖	mathematical	—	FreeGroup.reduceCyclically	—	List.bidirectionalRec_cons_append
isCyclicallyReduced 📖	mathematical	FreeGroup.IsReduced	FreeGroup.IsCyclicallyReduced FreeGroup.reduceCyclically	—	nil singleton cons_append FreeGroup.isCyclicallyReduced_cons_append_iff FreeGroup.IsReduced.infix
nil 📖	mathematical	—	FreeGroup.reduceCyclically	—	List.bidirectionalRec_nil
reduce_flatten_replicate 📖	mathematical	FreeGroup.IsReduced	FreeGroup.reduce conjugator FreeGroup.reduceCyclically FreeGroup.invRev	—	reduce_flatten_replicate_succ
reduce_flatten_replicate_succ 📖	mathematical	FreeGroup.IsReduced	FreeGroup.reduce conjugator FreeGroup.reduceCyclically FreeGroup.invRev	—	zero_add conj_conjugator_reduceCyclically FreeGroup.reduce_append_reduce_reduce FreeGroup.IsReduced.reduce_eq FreeGroup.reduce.sound Mathlib.Tactic.Group.zpow_trick_one' neg_add_cancel zpow_zero mul_one FreeGroup.isReduced_iff_reduce_eq FreeGroup.IsReduced.append_flatten_replicate_append isCyclicallyReduced
singleton 📖	mathematical	—	FreeGroup.reduceCyclically	—	List.bidirectionalRec_singleton

FreeGroup.reduceCyclically.conjugator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_append 📖	mathematical	—	FreeGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_cons_append
nil 📖	mathematical	—	FreeGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_nil
singleton 📖	mathematical	—	FreeGroup.reduceCyclically.conjugator	—	List.bidirectionalRec_singleton

---

← Back to Index