Reduce

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

Statistics

Metric	Count
Definitions instDecidableEq, norm, reduce, churchRosser, toWord, decidableRel, enum, instDecidableEq, instFintypeSubtypeListProdBoolRed, norm, reduce, churchRosser, toWord	13
Theorems of_reduce_eq, reduce_eq, reduce_left, reduce_right, instNontrivialOfNonempty, isReduced_iff_reduce_eq, isReduced_toWord, mk_toWord, norm_add_le, norm_eq_zero, norm_mk_le, norm_neg_eq, norm_of, norm_of_nsmul, norm_surjective, norm_zero, of_ne_zero, eq, cons, eq_of_red, exact, idem, min, not, red, rev, self, sound, reduce_append_reduce_reduce, reduce_cons_reduce, reduce_negRev, reduce_negRev_left_cancel, reduce_nil, reduce_replicate, reduce_singleton, reduce_toWord, toWord_add, toWord_add_sublist, toWord_eq_nil_iff, toWord_inj, toWord_injective, toWord_mk, toWord_neg, toWord_nsmul, toWord_of, toWord_of_nsmul, toWord_zero, zero_ne_of, of_reduce_eq, reduce_eq, complete, sound, reduce_left, reduce_right, reduce_eq, instNontrivialOfNonempty, isReduced_iff_reduce_eq, isReduced_toWord, mk_toWord, norm_eq_zero, norm_inv_eq, norm_mk_le, norm_mul_le, norm_of, norm_of_pow, norm_one, norm_surjective, of_ne_one, one_ne_of, reduce_eq, eq, cons, eq_of_red, exact, idem, min, not, red, rev, self, sound, reduce_append_reduce_reduce, reduce_cons_reduce, reduce_invRev, reduce_invRev_left_cancel, reduce_nil, reduce_replicate, reduce_singleton, reduce_toWord, toWord_eq_nil_iff, toWord_inj, toWord_injective, toWord_inv, toWord_mk, toWord_mul, toWord_mul_sublist, toWord_of, toWord_of_pow, toWord_one, toWord_pow	100
Total	113

FreeAddGroup

Definitions

Name	Category	Theorems
instDecidableEq 📖	CompOp	—
norm 📖	CompOp	8 math math: norm_of, norm_surjective, norm_eq_zero, norm_neg_eq, norm_zero, norm_mk_le, norm_add_le, norm_of_nsmul
reduce 📖	CompOp	26 math math: reduce_append_reduce_reduce, FreeGroup.freeAddGroup.red.reduce_eq, reduce_negRev_left_cancel, reduce_negRev, reduce.sound, reduce_nil, reduce.rev, reduce.idem, reduce_replicate, reduce_cons_reduce, Red.reduce_left, reduce_toWord, Red.reduce_right, IsReduced.reduce_eq, reduce.self, reduce.Step.eq, reduce.red, toWord_mk, reduceCyclically.reduce_flatten_replicate, reduceCyclically.reduce_flatten_replicate_succ, reduce_singleton, reduce.cons, toWord_nsmul, reduce.eq_of_red, toWord_add, isReduced_iff_reduce_eq
toWord 📖	CompOp	14 math math: toWord_of_nsmul, toWord_of, toWord_add_sublist, toWord_injective, toWord_inj, reduce_toWord, toWord_eq_nil_iff, mk_toWord, toWord_neg, isReduced_toWord, toWord_mk, toWord_zero, toWord_nsmul, toWord_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialOfNonempty 📖	mathematical	—	Nontrivial FreeAddGroup	—	zero_ne_of
isReduced_iff_reduce_eq 📖	mathematical	—	IsReduced reduce	—	IsReduced.reduce_eq IsReduced.of_reduce_eq
isReduced_toWord 📖	mathematical	—	IsReduced toWord	—	isReduced_iff_reduce_eq reduce_toWord
mk_toWord 📖	mathematical	—	toWord	—	reduce.self
norm_add_le 📖	mathematical	—	norm FreeAddGroup instAdd	—	mk_toWord norm_mk_le
norm_eq_zero 📖	mathematical	—	norm FreeAddGroup instZero	—	toWord_eq_nil_iff
norm_mk_le 📖	mathematical	—	norm	—	Red.length_le reduce.red
norm_neg_eq 📖	mathematical	—	norm FreeAddGroup instNeg	—	toWord_neg negRev_length
norm_of 📖	mathematical	—	norm of	—	—
norm_of_nsmul 📖	mathematical	—	norm FreeAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddGroup of	—	norm.eq_1 toWord_of_nsmul
norm_surjective 📖	mathematical	—	FreeAddGroup norm	—	norm_of_nsmul
norm_zero 📖	mathematical	—	norm FreeAddGroup instZero	—	—
of_ne_zero 📖	—	—	—	—	zero_ne_of
reduce_append_reduce_reduce 📖	mathematical	—	reduce	—	toWord_add
reduce_cons_reduce 📖	mathematical	—	reduce	—	reduce.idem
reduce_negRev 📖	mathematical	—	reduce negRev	—	reduce.min red_negRev_iff negRev_negRev Red.reduce_left Red.negRev reduce.red
reduce_negRev_left_cancel 📖	mathematical	—	reduce negRev	—	neg_add_cancel
reduce_nil 📖	mathematical	—	reduce	—	—
reduce_replicate 📖	mathematical	—	reduce	—	reduce.cons
reduce_singleton 📖	mathematical	—	reduce	—	—
reduce_toWord 📖	mathematical	—	reduce toWord	—	reduce.idem
toWord_add 📖	mathematical	—	toWord FreeAddGroup instAdd reduce	—	mk_toWord reduce_toWord
toWord_add_sublist 📖	mathematical	—	toWord FreeAddGroup instAdd	—	Red.sublist mk_toWord reduce.red
toWord_eq_nil_iff 📖	mathematical	—	toWord FreeAddGroup instZero	—	toWord_injective toWord_zero
toWord_inj 📖	mathematical	—	toWord	—	toWord_injective
toWord_injective 📖	mathematical	—	FreeAddGroup toWord	—	reduce.exact
toWord_mk 📖	mathematical	—	toWord reduce	—	—
toWord_neg 📖	mathematical	—	toWord FreeAddGroup instNeg negRev	—	reduce_negRev
toWord_nsmul 📖	mathematical	—	toWord FreeAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddGroup reduce	—	mk_toWord reduce_toWord
toWord_of 📖	mathematical	—	toWord of	—	—
toWord_of_nsmul 📖	mathematical	—	toWord FreeAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddGroup of	—	of.eq_1 reduce.Step.eq toWord.eq_1 reduce_replicate
toWord_zero 📖	mathematical	—	toWord FreeAddGroup instZero	—	—
zero_ne_of 📖	—	—	—	—	—

FreeAddGroup.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_reduce_eq 📖	mathematical	FreeAddGroup.reduce	FreeAddGroup.IsReduced	—	eq_1 List.isChain_iff_forall_rel_of_append_cons_cons Bool.ne_not FreeAddGroup.reduce.not
reduce_eq 📖	mathematical	FreeAddGroup.IsReduced	FreeAddGroup.reduce	—	red_iff_eq FreeAddGroup.reduce.red

FreeAddGroup.Red

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reduce_left 📖	mathematical	FreeAddGroup.Red	FreeAddGroup.reduce	—	FreeAddGroup.reduce.red FreeAddGroup.reduce.eq_of_red
reduce_right 📖	mathematical	FreeAddGroup.Red	FreeAddGroup.reduce	—	FreeAddGroup.reduce.red FreeAddGroup.reduce.eq_of_red

FreeAddGroup.reduce

Definitions

Name	Category	Theorems
churchRosser 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons 📖	mathematical	—	FreeAddGroup.reduce	—	—
eq_of_red 📖	mathematical	FreeAddGroup.Red	FreeAddGroup.reduce	—	FreeAddGroup.Red.church_rosser red FreeAddGroup.Red.trans min
exact 📖	—	FreeAddGroup.reduce	—	—	FreeAddGroup.Red.exact red
idem 📖	mathematical	—	FreeAddGroup.reduce	—	min red
min 📖	—	FreeAddGroup.Red FreeAddGroup.reduce	—	—	not
not 📖	—	FreeAddGroup.reduce	—	—	—
red 📖	mathematical	—	FreeAddGroup.Red FreeAddGroup.reduce	—	FreeAddGroup.Red.cons_cons FreeAddGroup.Red.trans FreeAddGroup.Red.Step.to_red FreeAddGroup.Red.Step.cons_not_rev
rev 📖	mathematical	FreeAddGroup.Red	FreeAddGroup.reduce	—	red eq_of_red
self 📖	mathematical	—	FreeAddGroup.reduce	—	exact idem
sound 📖	mathematical	—	FreeAddGroup.reduce	—	FreeAddGroup.Red.exact eq_of_red

FreeAddGroup.reduce.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	FreeAddGroup.Red.Step	FreeAddGroup.reduce	—	FreeAddGroup.Red.church_rosser FreeAddGroup.reduce.red Relation.ReflTransGen.head FreeAddGroup.reduce.min

FreeGroup

Definitions

Name	Category	Theorems
instDecidableEq 📖	CompOp	—
instFintypeSubtypeListProdBoolRed 📖	CompOp	—
norm 📖	CompOp	8 math math: norm_surjective, norm_of_pow, norm_mul_le, norm_mk_le, norm_one, norm_of, norm_eq_zero, norm_inv_eq
reduce 📖	CompOp	26 math math: reduce_invRev_left_cancel, Red.reduce_left, reduce.cons, reduce.eq_of_red, reduceCyclically.reduce_flatten_replicate_succ, reduce_append_reduce_reduce, reduce.sound, IsReduced.reduce_eq, toWord_pow, toWord_mk, isReduced_iff_reduce_eq, reduce_toWord, reduce_nil, reduce.self, Red.reduce_right, reduce.red, reduce_cons_reduce, reduce.idem, red.reduce_eq, reduce_replicate, reduce.rev, reduce_invRev, reduceCyclically.reduce_flatten_replicate, toWord_mul, reduce_singleton, reduce.Step.eq
toWord 📖	CompOp	14 math math: toWord_of_pow, toWord_mul_sublist, toWord_pow, toWord_mk, reduce_toWord, toWord_inv, mk_toWord, toWord_one, toWord_of, toWord_injective, isReduced_toWord, toWord_inj, toWord_mul, toWord_eq_nil_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialOfNonempty 📖	mathematical	—	Nontrivial FreeGroup	—	one_ne_of
isReduced_iff_reduce_eq 📖	mathematical	—	IsReduced reduce	—	IsReduced.reduce_eq IsReduced.of_reduce_eq
isReduced_toWord 📖	mathematical	—	IsReduced toWord	—	reduce_toWord
mk_toWord 📖	mathematical	—	toWord	—	reduce.self
norm_eq_zero 📖	mathematical	—	norm FreeGroup instOne	—	—
norm_inv_eq 📖	mathematical	—	norm FreeGroup instInv	—	toWord_inv invRev_length
norm_mk_le 📖	mathematical	—	norm	—	Red.length_le reduce.red
norm_mul_le 📖	mathematical	—	norm FreeGroup instMul	—	mk_toWord norm_mk_le
norm_of 📖	mathematical	—	norm of	—	—
norm_of_pow 📖	mathematical	—	norm FreeGroup Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup of	—	norm.eq_1 toWord_of_pow
norm_one 📖	mathematical	—	norm FreeGroup instOne	—	—
norm_surjective 📖	mathematical	—	FreeGroup norm	—	norm_of_pow
of_ne_one 📖	—	—	—	—	one_ne_of
one_ne_of 📖	—	—	—	—	—
reduce_append_reduce_reduce 📖	mathematical	—	reduce	—	toWord_mul
reduce_cons_reduce 📖	mathematical	—	reduce	—	reduce.idem
reduce_invRev 📖	mathematical	—	reduce invRev	—	reduce.min red_invRev_iff invRev_invRev Red.reduce_left Red.invRev reduce.red
reduce_invRev_left_cancel 📖	mathematical	—	reduce invRev	—	inv_mul_cancel
reduce_nil 📖	mathematical	—	reduce	—	—
reduce_replicate 📖	mathematical	—	reduce	—	reduce.cons
reduce_singleton 📖	mathematical	—	reduce	—	—
reduce_toWord 📖	mathematical	—	reduce toWord	—	reduce.idem
toWord_eq_nil_iff 📖	mathematical	—	toWord FreeGroup instOne	—	toWord_injective toWord_one
toWord_inj 📖	mathematical	—	toWord	—	toWord_injective
toWord_injective 📖	mathematical	—	FreeGroup toWord	—	reduce.exact
toWord_inv 📖	mathematical	—	toWord FreeGroup instInv invRev	—	reduce_invRev
toWord_mk 📖	mathematical	—	toWord reduce	—	—
toWord_mul 📖	mathematical	—	toWord FreeGroup instMul reduce	—	mk_toWord reduce_toWord
toWord_mul_sublist 📖	mathematical	—	toWord FreeGroup instMul	—	Red.sublist mk_toWord reduce.red
toWord_of 📖	mathematical	—	toWord of	—	—
toWord_of_pow 📖	mathematical	—	toWord FreeGroup Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup of	—	of.eq_1 reduce.Step.eq toWord.eq_1 reduce_replicate
toWord_one 📖	mathematical	—	toWord FreeGroup instOne	—	—
toWord_pow 📖	mathematical	—	toWord FreeGroup Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup reduce	—	mk_toWord reduce_toWord

FreeGroup.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_reduce_eq 📖	mathematical	FreeGroup.reduce	FreeGroup.IsReduced	—	eq_1 List.isChain_iff_forall_rel_of_append_cons_cons Bool.ne_not FreeGroup.reduce.not
reduce_eq 📖	mathematical	FreeGroup.IsReduced	FreeGroup.reduce	—	red_iff_eq FreeGroup.reduce.red

FreeGroup.Red

Definitions

Name	Category	Theorems
decidableRel 📖	CompOp	—
enum 📖	CompOp	1 math math: enum.complete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reduce_left 📖	mathematical	FreeGroup.Red	FreeGroup.reduce	—	FreeGroup.reduce.red FreeGroup.reduce.eq_of_red
reduce_right 📖	mathematical	FreeGroup.Red	FreeGroup.reduce	—	FreeGroup.reduce.red FreeGroup.reduce.eq_of_red

FreeGroup.Red.enum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete 📖	mathematical	FreeGroup.Red	FreeGroup.Red.enum	—	List.mem_filter_of_mem List.mem_sublists FreeGroup.Red.sublist
sound 📖	—	FreeGroup.Red	—	—	List.of_mem_filter

FreeGroup.freeAddGroup.red

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reduce_eq 📖	mathematical	FreeAddGroup.Red	FreeAddGroup.reduce	—	FreeAddGroup.reduce.eq_of_red

FreeGroup.red

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reduce_eq 📖	mathematical	FreeGroup.Red	FreeGroup.reduce	—	FreeGroup.reduce.eq_of_red

FreeGroup.reduce

Definitions

Name	Category	Theorems
churchRosser 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons 📖	mathematical	—	FreeGroup.reduce	—	—
eq_of_red 📖	mathematical	FreeGroup.Red	FreeGroup.reduce	—	FreeGroup.Red.church_rosser red FreeGroup.Red.trans min
exact 📖	—	FreeGroup.reduce	—	—	FreeGroup.Red.exact red
idem 📖	mathematical	—	FreeGroup.reduce	—	min red
min 📖	—	FreeGroup.Red FreeGroup.reduce	—	—	not
not 📖	—	FreeGroup.reduce	—	—	—
red 📖	mathematical	—	FreeGroup.Red FreeGroup.reduce	—	FreeGroup.Red.cons_cons FreeGroup.Red.trans FreeGroup.Red.Step.to_red FreeGroup.Red.Step.cons_not_rev
rev 📖	mathematical	FreeGroup.Red	FreeGroup.reduce	—	red eq_of_red
self 📖	mathematical	—	FreeGroup.reduce	—	exact idem
sound 📖	mathematical	—	FreeGroup.reduce	—	FreeGroup.Red.exact eq_of_red

FreeGroup.reduce.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	FreeGroup.Red.Step	FreeGroup.reduce	—	FreeGroup.Red.church_rosser FreeGroup.reduce.red Relation.ReflTransGen.head FreeGroup.reduce.min

---

← Back to Index