PushoutI

📁 Source: Mathlib/GroupTheory/PushoutI.lean

Statistics

Metric	Count
Definitions PushoutI, NormalWord, Pair, toPair, Transversal, baseAction, cons, consRecOn, empty, equiv, equivPair, head, instInhabited, instInhabitedPair, mulAction, prod, rcons, summandAction, toWord, base, con, homEquiv, instGroup, monoid, mul, of, ofCoprodI, one	28
Theorems normalized, compl, injective, one_mem, base_smul_def, base_smul_def', base_smul_eq_smul, cons_eq_smul, cons_head, cons_toList, empty_head, empty_toList, eq_one_of_smul_normalized, ext, ext_iff, ext_smul, instFaithfulSMul, instFaithfulSMul_1, instFaithfulSMul_2, normalized, of_smul_eq_smul, prod_base_smul, prod_cons, prod_empty, prod_injective, prod_smul, prod_smul_empty, prod_summand_smul, rcons_injective, summand_smul_def, summand_smul_def', transversal_nonempty, eq_empty_of_mem_range, exists_normalWord_prod_eq, base_injective, homEquiv_apply_coe, homEquiv_symm_apply, hom_ext, hom_ext_iff, hom_ext_nonempty, hom_ext_nonempty_iff, induction_on, inf_of_range_eq_base_range, lift_base, lift_of, ofCoprodI_of, of_apply_eq_base, of_comp_eq_base, of_injective	49
Total	77

Monoid

Definitions

Name	Category	Theorems
PushoutI 📖	CompOp	26 math math: PushoutI.hom_ext_iff, PushoutI.NormalWord.base_smul_def, PushoutI.NormalWord.base_smul_eq_smul, PushoutI.of_comp_eq_base, PushoutI.NormalWord.prod_cons, PushoutI.NormalWord.instFaithfulSMul, PushoutI.of_apply_eq_base, PushoutI.lift_base, PushoutI.NormalWord.prod_summand_smul, PushoutI.NormalWord.prod_base_smul, PushoutI.homEquiv_symm_apply, PushoutI.base_injective, PushoutI.NormalWord.prod_smul_empty, PushoutI.ofCoprodI_of, PushoutI.homEquiv_apply_coe, PushoutI.inf_of_range_eq_base_range, PushoutI.of_injective, PushoutI.Reduced.exists_normalWord_prod_eq, PushoutI.hom_ext_nonempty_iff, PushoutI.NormalWord.prod_empty, PushoutI.NormalWord.cons_eq_smul, PushoutI.NormalWord.of_smul_eq_smul, PushoutI.NormalWord.prod_injective, PushoutI.NormalWord.prod_smul, PushoutI.NormalWord.summand_smul_def, PushoutI.lift_of

Monoid.PushoutI

Definitions

Name	Category	Theorems
NormalWord 📖	CompData	16 math math: NormalWord.base_smul_def, NormalWord.base_smul_eq_smul, NormalWord.base_smul_def', NormalWord.instFaithfulSMul, NormalWord.prod_summand_smul, NormalWord.prod_base_smul, NormalWord.prod_smul_empty, NormalWord.summand_smul_def', NormalWord.cons_eq_smul, NormalWord.of_smul_eq_smul, NormalWord.instFaithfulSMul_2, NormalWord.prod_injective, NormalWord.prod_smul, NormalWord.summand_smul_def, NormalWord.instFaithfulSMul_1, NormalWord.rcons_injective
base 📖	CompOp	10 math math: hom_ext_iff, NormalWord.base_smul_def, NormalWord.base_smul_eq_smul, of_comp_eq_base, of_apply_eq_base, lift_base, NormalWord.prod_base_smul, base_injective, homEquiv_apply_coe, inf_of_range_eq_base_range
con 📖	CompOp	—
homEquiv 📖	CompOp	2 math math: homEquiv_symm_apply, homEquiv_apply_coe
instGroup 📖	CompOp	1 math math: inf_of_range_eq_base_range
monoid 📖	CompOp	23 math math: hom_ext_iff, NormalWord.base_smul_def, NormalWord.base_smul_eq_smul, of_comp_eq_base, NormalWord.prod_cons, NormalWord.instFaithfulSMul, of_apply_eq_base, lift_base, NormalWord.prod_summand_smul, NormalWord.prod_base_smul, homEquiv_symm_apply, base_injective, NormalWord.prod_smul_empty, ofCoprodI_of, homEquiv_apply_coe, of_injective, Reduced.exists_normalWord_prod_eq, hom_ext_nonempty_iff, NormalWord.cons_eq_smul, NormalWord.of_smul_eq_smul, NormalWord.prod_smul, NormalWord.summand_smul_def, lift_of
mul 📖	CompOp	4 math math: NormalWord.prod_cons, NormalWord.prod_summand_smul, NormalWord.prod_base_smul, NormalWord.prod_smul
of 📖	CompOp	14 math math: hom_ext_iff, of_comp_eq_base, NormalWord.prod_cons, of_apply_eq_base, NormalWord.prod_summand_smul, ofCoprodI_of, homEquiv_apply_coe, inf_of_range_eq_base_range, of_injective, hom_ext_nonempty_iff, NormalWord.cons_eq_smul, NormalWord.of_smul_eq_smul, NormalWord.summand_smul_def, lift_of
ofCoprodI 📖	CompOp	2 math math: ofCoprodI_of, Reduced.exists_normalWord_prod_eq
one 📖	CompOp	1 math math: NormalWord.prod_empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_injective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Monoid.PushoutI monoid base	—	NormalWord.transversal_nonempty Function.Injective.of_comp FaithfulSMul.eq_of_smul_eq_smul NormalWord.instFaithfulSMul_2 NormalWord.base_smul_eq_smul
homEquiv_apply_coe 📖	mathematical	—	MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DFunLike.coe Equiv Monoid.PushoutI monoid EquivLike.toFunLike Equiv.instEquivLike homEquiv MonoidHom.comp of base	—	—
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Monoid.PushoutI monoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv lift	—	—
hom_ext 📖	—	MonoidHom.comp Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid of base	—	—	MonoidHom.cancel_right Con.mk'_surjective Monoid.Coprod.hom_ext Monoid.CoprodI.ext_hom
hom_ext_iff 📖	mathematical	—	MonoidHom.comp Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid of base	—	hom_ext
hom_ext_nonempty 📖	—	MonoidHom.comp Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid of	—	—	hom_ext MonoidHom.ext of_comp_eq_base MonoidHom.comp_assoc
hom_ext_nonempty_iff 📖	mathematical	—	MonoidHom.comp Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid of	—	hom_ext_nonempty
induction_on 📖	—	DFunLike.coe MonoidHom Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike of base mul	—	—	Con.induction_on Monoid.Coprod.induction_on Monoid.CoprodI.induction_on map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass map_mul MonoidHomClass.toMulHomClass
inf_of_range_eq_base_range 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Subgroup Monoid.PushoutI instGroup Subgroup.instMin MonoidHom.range of base	—	le_antisymm SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass MonoidHom.mem_range of_apply_eq_base SubgroupClass.toInvMemClass Reduced.eq_empty_of_mem_range map_inv mul_one map_mul MonoidHomClass.toMulHomClass ofCoprodI_of mul_inv_cancel le_inf of_comp_eq_base
lift_base 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass	DFunLike.coe MonoidHom Monoid.PushoutI monoid MonoidHom.instFunLike lift base	—	—
lift_of 📖	mathematical	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass	DFunLike.coe MonoidHom Monoid.PushoutI monoid MonoidHom.instFunLike lift of	—	Monoid.CoprodI.lift_of
ofCoprodI_of 📖	mathematical	—	DFunLike.coe MonoidHom Monoid.CoprodI Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass Monoid.instCoprodI monoid MonoidHom.instFunLike ofCoprodI Monoid.CoprodI.of of	—	Monoid.CoprodI.lift_of
of_apply_eq_base 📖	mathematical	—	DFunLike.coe MonoidHom Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid MonoidHom.instFunLike of base	—	MonoidHom.comp_apply of_comp_eq_base
of_comp_eq_base 📖	mathematical	—	MonoidHom.comp Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass monoid of base	—	MonoidHom.ext Con.eq
of_injective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Monoid.PushoutI monoid of	—	NormalWord.transversal_nonempty Function.Injective.of_comp FaithfulSMul.eq_of_smul_eq_smul NormalWord.instFaithfulSMul_1 NormalWord.of_smul_eq_smul

Monoid.PushoutI.NormalWord

Definitions

Name	Category	Theorems
Pair 📖	CompData	3 math math: summand_smul_def', summand_smul_def, rcons_injective
Transversal 📖	CompData	1 math math: transversal_nonempty
baseAction 📖	CompOp	4 math math: base_smul_eq_smul, base_smul_def', prod_base_smul, instFaithfulSMul_2
cons 📖	CompOp	4 math math: prod_cons, cons_head, cons_eq_smul, cons_toList
consRecOn 📖	CompOp	—
empty 📖	CompOp	4 math math: prod_smul_empty, prod_empty, empty_head, empty_toList
equiv 📖	CompOp	—
equivPair 📖	CompOp	2 math math: summand_smul_def', summand_smul_def
head 📖	CompOp	6 math math: base_smul_def, base_smul_def', cons_head, ext_iff, empty_head, cons_toList
instInhabited 📖	CompOp	—
instInhabitedPair 📖	CompOp	—
mulAction 📖	CompOp	8 math math: base_smul_def, base_smul_eq_smul, instFaithfulSMul, prod_smul_empty, cons_eq_smul, of_smul_eq_smul, prod_smul, summand_smul_def
prod 📖	CompOp	8 math math: prod_cons, prod_summand_smul, prod_base_smul, prod_smul_empty, Monoid.PushoutI.Reduced.exists_normalWord_prod_eq, prod_empty, prod_injective, prod_smul
rcons 📖	CompOp	1 math math: rcons_injective
summandAction 📖	CompOp	4 math math: prod_summand_smul, summand_smul_def', of_smul_eq_smul, instFaithfulSMul_1
toWord 📖	CompOp	6 math math: base_smul_def, base_smul_def', Monoid.PushoutI.Reduced.exists_normalWord_prod_eq, ext_iff, empty_toList, cons_toList

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_smul_def 📖	mathematical	—	Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.PushoutI.base toWord MulOne.toMul head normalized	—	—
base_smul_def' 📖	mathematical	—	Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction baseAction toWord MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass head normalized	—	—
base_smul_eq_smul 📖	mathematical	—	Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.PushoutI.base baseAction	—	normalized base_smul_def base_smul_def'
cons_eq_smul 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range	cons Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.PushoutI.of	—	ext_smul Transversal.compl Transversal.injective Monoid.CoprodI.Word.cons_eq_smul MonoidHom.apply_ofInjective_symm Subgroup.IsComplement.equiv_fst_eq_mul_inv mul_assoc map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv SemigroupAction.mul_smul inv_smul_smul Monoid.CoprodI.Word.Pair.fstIdx_ne Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul Pair.normalized Monoid.CoprodI.Word.rcons_eq_smul smul_inv_smul
cons_head 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range	head cons DFunLike.coe MulEquiv Subgroup.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm MonoidHom.ofInjective Transversal.injective Set.Elem Set.range MonoidHom MonoidHom.instFunLike Transversal.set Equiv Equiv.instEquivLike Subgroup.IsComplement.equiv Transversal.compl	—	—
cons_toList 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range	Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid toWord cons Set Set.instMembership Transversal.set Set.Elem Set.range DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Subgroup.IsComplement.equiv Transversal.compl MulOne.toMul head	—	—
empty_head 📖	mathematical	—	head empty InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
empty_toList 📖	mathematical	—	Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid toWord empty	—	—
eq_one_of_smul_normalized 📖	mathematical	Set Set.instMembership Transversal.set	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Transversal.compl Exists.fst Exists.snd Monoid.CoprodI.Word.equivPair_head Subgroup.IsComplement.equiv_snd_eq_self_iff_mem OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Transversal.one_mem Subgroup.IsComplement.equiv_one LeftCancelSemigroup.toIsLeftCancelMul Subgroup.IsComplement.equiv_mul_left_of_mem injective_iff_map_eq_one' MonoidHom.instMonoidHomClass Transversal.injective mul_one Sigma.eta RightCancelSemigroup.toIsRightCancelMul
ext 📖	—	head Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid toWord	—	—	—
ext_iff 📖	mathematical	—	head Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid toWord	—	ext
ext_smul 📖	—	Monoid.CoprodI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.CoprodI.Word SemigroupAction.toSMul Monoid.toSemigroup Monoid.instCoprodI MulAction.toSemigroupAction Monoid.CoprodI.Word.instMulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.CoprodI.of head toWord	—	—	eq_one_of_smul_normalized MonoidHom.instMonoidHomClass MonoidHomClass.toMulHomClass inv_mul_cancel one_smul inv_mul_eq_one SemigroupAction.mul_smul smul_eq_iff_eq_inv_smul
instFaithfulSMul 📖	mathematical	—	FaithfulSMul Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction	—	prod_smul prod_empty mul_one
instFaithfulSMul_1 📖	mathematical	—	FaithfulSMul Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction summandAction	—	Monoid.CoprodI.Word.Pair.fstIdx_ne Pair.normalized EquivLike.toEmbeddingLike RightCancelSemigroup.toIsRightCancelMul
instFaithfulSMul_2 📖	mathematical	—	FaithfulSMul Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction baseAction	—	normalized RightCancelSemigroup.toIsRightCancelMul
normalized 📖	mathematical	Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid toWord	Set Set.instMembership Transversal.set	—	—
of_smul_eq_smul 📖	mathematical	—	Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.PushoutI.of summandAction	—	Monoid.CoprodI.Word.Pair.fstIdx_ne Pair.normalized summand_smul_def summand_smul_def'
prod_base_smul 📖	mathematical	—	prod Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction baseAction Monoid.PushoutI Monoid.PushoutI.mul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Monoid.PushoutI.monoid MonoidHom.instFunLike Monoid.PushoutI.base	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_assoc
prod_cons 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range	prod cons Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.mul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Monoid.PushoutI.monoid MonoidHom.instFunLike Monoid.PushoutI.of	—	Transversal.compl Transversal.injective Monoid.PushoutI.of_apply_eq_base MonoidHom.apply_ofInjective_symm Subgroup.IsComplement.equiv_fst_eq_mul_inv mul_assoc map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv Monoid.CoprodI.Word.prod_cons Monoid.PushoutI.ofCoprodI_of inv_mul_cancel_left
prod_empty 📖	mathematical	—	prod empty Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.one	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
prod_injective 📖	mathematical	—	Monoid.PushoutI.NormalWord Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid prod	—	Equiv.injective
prod_smul 📖	mathematical	—	prod Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction Monoid.PushoutI.mul	—	Monoid.PushoutI.induction_on of_smul_eq_smul prod_summand_smul base_smul_eq_smul prod_base_smul SemigroupAction.mul_smul mul_assoc
prod_smul_empty 📖	mathematical	—	Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction prod empty	—	prod_empty one_smul prod_cons SemigroupAction.mul_smul cons_eq_smul prod_smul
prod_summand_smul 📖	mathematical	—	prod Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction summandAction Monoid.PushoutI Monoid.PushoutI.mul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Monoid.PushoutI.monoid MonoidHom.instFunLike Monoid.PushoutI.of	—	Transversal.compl Transversal.injective Monoid.CoprodI.Word.Pair.fstIdx_ne Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul Monoid.CoprodI.Word.equivPair_smul_same Pair.normalized Monoid.CoprodI.Word.rcons_eq_smul Monoid.PushoutI.of_apply_eq_base MonoidHom.apply_ofInjective_symm Subgroup.IsComplement.equiv_fst_eq_mul_inv mul_assoc map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv Monoid.CoprodI.Word.prod_smul Monoid.PushoutI.ofCoprodI_of inv_mul_cancel_left mul_inv_cancel_left
rcons_injective 📖	mathematical	—	Pair Monoid.PushoutI.NormalWord rcons	—	Transversal.compl Transversal.injective EquivLike.toEmbeddingLike Subgroup.IsComplement.equiv_fst_mul_equiv_snd
summand_smul_def 📖	mathematical	—	Monoid.PushoutI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup Monoid.PushoutI.monoid MulAction.toSemigroupAction mulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Monoid.PushoutI.of Equiv Pair EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivPair	—	—
summand_smul_def' 📖	mathematical	—	Monoid.PushoutI.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction summandAction DFunLike.coe Equiv Pair EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivPair	—	—
transversal_nonempty 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Transversal	—	Subgroup.exists_isComplement_right

Monoid.PushoutI.NormalWord.Pair

Definitions

Name	Category	Theorems
toPair 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalized 📖	mathematical	Monoid.CoprodI.Word.toList DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.CoprodI.Word.Pair.tail toPair	Set Set.instMembership Monoid.PushoutI.NormalWord.Transversal.set	—	—

Monoid.PushoutI.NormalWord.Transversal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	—	Subgroup.IsComplement SetLike.coe Subgroup Subgroup.instSetLike MonoidHom.range set	—	—
injective 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	—	—
one_mem 📖	mathematical	—	Set Set.instMembership set InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

Monoid.PushoutI.Reduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_empty_of_mem_range 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike Monoid.PushoutI.Reduced Monoid.PushoutI Subgroup Monoid.PushoutI.instGroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range Monoid.PushoutI.base Monoid.CoprodI Monoid.instCoprodI Monoid.PushoutI.monoid Monoid.PushoutI.ofCoprodI Monoid.CoprodI.Word.prod	Monoid.CoprodI.Word.empty	—	Monoid.PushoutI.NormalWord.transversal_nonempty exists_normalWord_prod_eq instIsEmptyFalse map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one Monoid.PushoutI.NormalWord.prod_injective Monoid.CoprodI.Word.ext Nat.instCanonicallyOrderedAdd
exists_normalWord_prod_eq 📖	mathematical	Monoid.PushoutI.Reduced	Monoid.PushoutI.NormalWord.prod DFunLike.coe MonoidHom Monoid.CoprodI DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.PushoutI MulOneClass.toMulOne Monoid.toMulOneClass Monoid.instCoprodI Monoid.PushoutI.monoid MonoidHom.instFunLike Monoid.PushoutI.ofCoprodI Monoid.CoprodI.Word.prod Monoid.CoprodI.Word.toList Monoid.PushoutI.NormalWord.toWord	—	Monoid.PushoutI.NormalWord.prod_empty map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass Monoid.CoprodI.Word.fstIdx.eq_1 Monoid.PushoutI.NormalWord.prod_cons Monoid.CoprodI.Word.prod_cons map_mul MonoidHomClass.toMulHomClass Monoid.PushoutI.ofCoprodI_of

---

← Back to Index