HNNExtension

📁 Source: Mathlib/GroupTheory/HNNExtension.lean

Statistics

Metric	Count
Definitions HNNExtension, NormalWord, Cancels, ReducedWord, empty, head, prod, toList, TransversalPair, cons, consRecOn, empty, equiv, instInhabited, instMulAction, instMulAction_1, ofGroup, toReducedWord, unitsSMul, unitsSMulEquiv, unitsSMulGroup, unitsSMulWithCancel, con, of, t, toSubgroup, toSubgroupEquiv, instGroupHNNExtension	28
Theorems chain, empty_head, empty_toList, compl, nonempty, consRecOn_cons, consRecOn_ofGroup, cons_head, cons_toList, empty_head, empty_toList, ext, ext_iff, group_smul_def, group_smul_head, group_smul_toList, instFaithfulSMul, instFaithfulSMul_1, mem_set, not_cancels_of_cons_hyp, ofGroup_head, ofGroup_toList, of_smul_eq_smul, prod_cons, prod_empty, prod_group_smul, prod_injective, prod_smul, prod_smul_empty, prod_unitsSMul, smul_cons, smul_ofGroup, t_pow_smul_eq_unitsSMul, t_smul_eq_unitsSMul, unitsSMulEquiv_apply, unitsSMulEquiv_symm_apply, unitsSMulGroup_snd, unitsSMul_cancels_iff, unitsSMul_neg, unitsSMul_one_group_smul, exists_normalWord_prod_eq, map_fst_eq_and_of_prod_eq, toList_eq_nil_of_mem_of_range, equiv_eq_conj, equiv_symm_eq_conj, hom_ext, hom_ext_iff, induction_on, inv_t_mul_of, lift_of, lift_t, of_injective, of_mul_inv_t, of_mul_t, t_mul_of, toSubgroupEquiv_neg_apply, toSubgroupEquiv_neg_one, toSubgroupEquiv_one, toSubgroup_neg_one, toSubgroup_one	60
Total	88

HNNExtension

Definitions

Name	Category	Theorems
NormalWord 📖	CompData	17 math math: NormalWord.prod_group_smul, NormalWord.group_smul_toList, NormalWord.t_smul_eq_unitsSMul, NormalWord.prod_smul, NormalWord.smul_ofGroup, NormalWord.unitsSMul_one_group_smul, NormalWord.prod_injective, NormalWord.instFaithfulSMul_1, NormalWord.group_smul_def, NormalWord.instFaithfulSMul, NormalWord.group_smul_head, NormalWord.smul_cons, NormalWord.unitsSMulEquiv_symm_apply, NormalWord.of_smul_eq_smul, NormalWord.prod_smul_empty, NormalWord.unitsSMulEquiv_apply, NormalWord.t_pow_smul_eq_unitsSMul
con 📖	CompOp	—
of 📖	CompOp	12 math math: NormalWord.prod_group_smul, lift_of, equiv_eq_conj, NormalWord.prod_cons, inv_t_mul_of, of_mul_t, of_mul_inv_t, t_mul_of, hom_ext_iff, of_injective, NormalWord.of_smul_eq_smul, equiv_symm_eq_conj
t 📖	CompOp	12 math math: NormalWord.t_smul_eq_unitsSMul, equiv_eq_conj, NormalWord.prod_cons, inv_t_mul_of, NormalWord.prod_unitsSMul, of_mul_t, of_mul_inv_t, lift_t, t_mul_of, hom_ext_iff, equiv_symm_eq_conj, NormalWord.t_pow_smul_eq_unitsSMul
toSubgroup 📖	CompOp	7 math math: toSubgroup_neg_one, toSubgroup_one, NormalWord.unitsSMulGroup_snd, toSubgroupEquiv_neg_apply, ReducedWord.map_fst_eq_and_of_prod_eq, NormalWord.TransversalPair.compl, ReducedWord.exists_normalWord_prod_eq
toSubgroupEquiv 📖	CompOp	3 math math: toSubgroupEquiv_neg_one, toSubgroupEquiv_neg_apply, toSubgroupEquiv_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_eq_conj 📖	mathematical	—	DFunLike.coe MonoidHom HNNExtension MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulOne.toMul t InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	t_mul_of mul_inv_cancel_right
equiv_symm_eq_conj 📖	mathematical	—	DFunLike.coe MonoidHom HNNExtension MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid t	—	mul_assoc of_mul_t inv_mul_cancel_left
hom_ext 📖	—	MonoidHom.comp HNNExtension MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension of DFunLike.coe MonoidHom MonoidHom.instFunLike t	—	—	MonoidHom.cancel_right Con.mk'_surjective Monoid.Coprod.hom_ext MonoidHom.ext_mint
hom_ext_iff 📖	mathematical	—	MonoidHom.comp HNNExtension MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension of DFunLike.coe MonoidHom MonoidHom.instFunLike t	—	hom_ext
induction_on 📖	—	DFunLike.coe MonoidHom HNNExtension MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MonoidHom.instFunLike of t MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass MulMemClass.mul_mem equiv_eq_conj mul_assoc inv_mul_cancel mul_one hom_ext MonoidHom.ext lift_of MonoidHom.CompTriple.comp_eq MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId lift_t
inv_t_mul_of 📖	mathematical	—	HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid t DFunLike.coe MonoidHom MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm	—	equiv_symm_eq_conj mul_inv_cancel_right
lift_of 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MonoidHom.instFunLike Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike	HNNExtension instGroupHNNExtension lift of	—	—
lift_t 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MonoidHom.instFunLike Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike	HNNExtension instGroupHNNExtension lift t	—	zpow_one
of_injective 📖	mathematical	—	HNNExtension DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MonoidHom.instFunLike of	—	NormalWord.TransversalPair.nonempty Function.Injective.of_comp FaithfulSMul.eq_of_smul_eq_smul NormalWord.instFaithfulSMul NormalWord.of_smul_eq_smul
of_mul_inv_t 📖	mathematical	—	HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension DFunLike.coe MonoidHom MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid t MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike	—	equiv_eq_conj mul_assoc inv_mul_cancel_left
of_mul_t 📖	mathematical	—	HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension DFunLike.coe MonoidHom MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike t MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm	—	t_mul_of MulEquiv.apply_symm_apply
t_mul_of 📖	mathematical	—	HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension t DFunLike.coe MonoidHom MonoidHom.instFunLike of Subgroup SetLike.instMembership Subgroup.instSetLike MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike	—	Con.eq
toSubgroupEquiv_neg_apply 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike toSubgroupEquiv	—	Int.units_eq_one_or MulEquiv.symm_apply_apply MulEquiv.apply_symm_apply
toSubgroupEquiv_neg_one 📖	mathematical	—	toSubgroupEquiv Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne MulEquiv.symm Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.mul	—	—
toSubgroupEquiv_one 📖	mathematical	—	toSubgroupEquiv Units Int.instMonoid Units.instOne	—	—
toSubgroup_neg_one 📖	mathematical	—	toSubgroup Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	—
toSubgroup_one 📖	mathematical	—	toSubgroup Units Int.instMonoid Units.instOne	—	—

HNNExtension.NormalWord

Definitions

Name	Category	Theorems
Cancels 📖	MathDef	2 math math: unitsSMul_cancels_iff, not_cancels_of_cons_hyp
ReducedWord 📖	CompData	—
TransversalPair 📖	CompData	1 math math: TransversalPair.nonempty
cons 📖	CompOp	5 math math: prod_cons, consRecOn_cons, smul_cons, cons_toList, cons_head
consRecOn 📖	CompOp	2 math math: consRecOn_cons, consRecOn_ofGroup
empty 📖	CompOp	4 math math: empty_head, prod_empty, empty_toList, prod_smul_empty
equiv 📖	CompOp	—
instInhabited 📖	CompOp	—
instMulAction 📖	CompOp	9 math math: prod_group_smul, group_smul_toList, smul_ofGroup, unitsSMul_one_group_smul, group_smul_def, instFaithfulSMul, group_smul_head, smul_cons, of_smul_eq_smul
instMulAction_1 📖	CompOp	6 math math: t_smul_eq_unitsSMul, prod_smul, instFaithfulSMul_1, of_smul_eq_smul, prod_smul_empty, t_pow_smul_eq_unitsSMul
ofGroup 📖	CompOp	4 math math: smul_ofGroup, ofGroup_head, consRecOn_ofGroup, ofGroup_toList
toReducedWord 📖	CompOp	15 math math: prod_group_smul, group_smul_toList, prod_smul, prod_unitsSMul, ext_iff, empty_head, prod_injective, group_smul_def, group_smul_head, prod_empty, empty_toList, ofGroup_head, prod_smul_empty, ofGroup_toList, HNNExtension.ReducedWord.exists_normalWord_prod_eq
unitsSMul 📖	CompOp	8 math math: t_smul_eq_unitsSMul, prod_unitsSMul, unitsSMul_cancels_iff, unitsSMul_one_group_smul, unitsSMul_neg, unitsSMulEquiv_symm_apply, unitsSMulEquiv_apply, t_pow_smul_eq_unitsSMul
unitsSMulEquiv 📖	CompOp	2 math math: unitsSMulEquiv_symm_apply, unitsSMulEquiv_apply
unitsSMulGroup 📖	CompOp	1 math math: unitsSMulGroup_snd
unitsSMulWithCancel 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
consRecOn_cons 📖	mathematical	Set Set.instMembership TransversalPair.set ReducedWord.head toReducedWord	consRecOn cons	—	—
consRecOn_ofGroup 📖	mathematical	—	consRecOn ofGroup	—	—
cons_head 📖	mathematical	Set Set.instMembership TransversalPair.set ReducedWord.head toReducedWord	cons	—	—
cons_toList 📖	mathematical	Set Set.instMembership TransversalPair.set ReducedWord.head toReducedWord	ReducedWord.toList cons Units Int.instMonoid	—	—
empty_head 📖	mathematical	—	ReducedWord.head toReducedWord empty InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
empty_toList 📖	mathematical	—	ReducedWord.toList toReducedWord empty Units Int.instMonoid	—	—
ext 📖	—	ReducedWord.head toReducedWord ReducedWord.toList	—	—	—
ext_iff 📖	mathematical	—	ReducedWord.head toReducedWord ReducedWord.toList	—	ext
group_smul_def 📖	mathematical	—	HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass ReducedWord.head toReducedWord ReducedWord.toList ReducedWord.chain mem_set	—	—
group_smul_head 📖	mathematical	—	ReducedWord.head toReducedWord HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
group_smul_toList 📖	mathematical	—	ReducedWord.toList toReducedWord HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction	—	—
instFaithfulSMul 📖	mathematical	—	FaithfulSMul HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction	—	ReducedWord.chain mem_set RightCancelSemigroup.toIsRightCancelMul
instFaithfulSMul_1 📖	mathematical	—	FaithfulSMul HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1	—	prod_smul prod_empty mul_one
mem_set 📖	mathematical	Units Int.instMonoid ReducedWord.toList toReducedWord	Set Set.instMembership TransversalPair.set	—	—
not_cancels_of_cons_hyp 📖	mathematical	—	Cancels	—	Int.instCharZero
ofGroup_head 📖	mathematical	—	ReducedWord.head toReducedWord ofGroup	—	—
ofGroup_toList 📖	mathematical	—	ReducedWord.toList toReducedWord ofGroup Units Int.instMonoid	—	—
of_smul_eq_smul 📖	mathematical	—	HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1 DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike HNNExtension.of instMulAction	—	mem_set HNNExtension.lift_of
prod_cons 📖	mathematical	Set Set.instMembership TransversalPair.set ReducedWord.head toReducedWord	ReducedWord.prod cons HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension DFunLike.coe MonoidHom MonoidHom.instFunLike HNNExtension.of DivInvMonoid.toZPow HNNExtension.t Units.val Int.instMonoid	—	mul_assoc
prod_empty 📖	mathematical	—	ReducedWord.prod toReducedWord empty HNNExtension InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupHNNExtension	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
prod_group_smul 📖	mathematical	—	ReducedWord.prod toReducedWord HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instGroupHNNExtension DFunLike.coe MonoidHom MonoidHom.instFunLike HNNExtension.of	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_assoc
prod_injective 📖	mathematical	—	HNNExtension.NormalWord HNNExtension ReducedWord.prod toReducedWord	—	Equiv.injective
prod_smul 📖	mathematical	—	ReducedWord.prod toReducedWord HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1 MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	HNNExtension.induction_on of_smul_eq_smul prod_group_smul t_smul_eq_unitsSMul prod_unitsSMul zpow_one SemigroupAction.mul_smul mul_assoc LeftCancelSemigroup.toIsLeftCancelMul smul_inv_smul mul_inv_cancel_left
prod_smul_empty 📖	mathematical	—	HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1 ReducedWord.prod toReducedWord empty	—	ReducedWord.chain mem_set mul_one of_smul_eq_smul prod_cons mul_assoc SemigroupAction.mul_smul t_pow_smul_eq_unitsSMul unitsSMul.eq_1 not_cancels_of_cons_hyp OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass TransversalPair.compl Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem cons.congr_simp ext LeftCancelSemigroup.toIsLeftCancelMul EquivLike.toEmbeddingLike MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass inv_mul_cancel_right Subgroup.IsComplement.equiv_snd_eq_inv_mul inv_one one_mul
prod_unitsSMul 📖	mathematical	—	ReducedWord.prod toReducedWord unitsSMul HNNExtension MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension DivInvMonoid.toZPow HNNExtension.t Units.val Int.instMonoid	—	unitsSMul.eq_1 prod_group_smul prod_cons zpow_neg Int.units_eq_one_or HNNExtension.equiv_eq_conj mul_assoc zpow_one inv_inv TransversalPair.compl map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv inv_mul_cancel_left LeftCancelSemigroup.toIsLeftCancelMul Subgroup.IsComplement.equiv_snd_eq_inv_mul mul_inv_cancel_left HNNExtension.equiv_symm_eq_conj
smul_cons 📖	mathematical	Set Set.instMembership TransversalPair.set ReducedWord.head toReducedWord	HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction cons MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
smul_ofGroup 📖	mathematical	—	HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction ofGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
t_pow_smul_eq_unitsSMul 📖	mathematical	—	HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1 DivInvMonoid.toZPow HNNExtension.t Units.val Int.instMonoid unitsSMul	—	Int.units_eq_one_or zpow_one HNNExtension.lift_t zpow_neg map_inv MonoidHom.instMonoidHomClass
t_smul_eq_unitsSMul 📖	mathematical	—	HNNExtension HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroupHNNExtension MulAction.toSemigroupAction instMulAction_1 HNNExtension.t unitsSMul Units Int.instMonoid Units.instOne	—	HNNExtension.lift_t
unitsSMulEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv HNNExtension.NormalWord EquivLike.toFunLike Equiv.instEquivLike unitsSMulEquiv unitsSMul Units Int.instMonoid Units.instOne	—	—
unitsSMulEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv HNNExtension.NormalWord EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitsSMulEquiv unitsSMul Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	—
unitsSMulGroup_snd 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike HNNExtension.toSubgroup Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Set.Elem TransversalPair.set unitsSMulGroup SetLike.coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Subgroup.IsComplement.equiv TransversalPair.compl	—	TransversalPair.compl Int.units_eq_one_or
unitsSMul_cancels_iff 📖	mathematical	—	Cancels Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing unitsSMul	—	neg_neg not_cancels_of_cons_hyp inv_mul_cancel_right
unitsSMul_neg 📖	mathematical	—	unitsSMul Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	unitsSMul.eq_1 unitsSMul_cancels_iff unitsSMulWithCancel.congr_simp TransversalPair.compl Subgroup.IsComplement.equiv_snd_eq_inv_mul mul_inv_cancel_right cons.congr_simp Subtype.coe_eta HNNExtension.toSubgroupEquiv_neg_apply smul_inv_smul mul_inv_rev SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem OneMemClass.one_mem ext Subgroup.IsComplement.equiv_mul_left map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Submonoid.coe_mul map_one MonoidHomClass.toOneHomClass mul_one inv_one one_mul mul_inv_cancel_left inv_mul_cancel_left
unitsSMul_one_group_smul 📖	mathematical	—	unitsSMul Units Int.instMonoid Units.instOne HNNExtension.NormalWord SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulAction Subgroup SetLike.instMembership Subgroup.instSetLike DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike	—	mul_inv_rev cons.congr_simp SemigroupAction.mul_smul Subgroup.coe_mul map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass TransversalPair.compl mul_assoc inv_mul_cancel mul_one Subgroup.IsComplement.equiv_mul_left

HNNExtension.NormalWord.ReducedWord

Definitions

Name	Category	Theorems
empty 📖	CompOp	2 math math: empty_head, empty_toList
head 📖	CompOp	8 math math: empty_head, HNNExtension.NormalWord.ext_iff, HNNExtension.NormalWord.empty_head, HNNExtension.NormalWord.group_smul_def, HNNExtension.NormalWord.group_smul_head, HNNExtension.NormalWord.ofGroup_head, HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq, HNNExtension.ReducedWord.exists_normalWord_prod_eq
prod 📖	CompOp	8 math math: HNNExtension.NormalWord.prod_group_smul, HNNExtension.NormalWord.prod_cons, HNNExtension.NormalWord.prod_smul, HNNExtension.NormalWord.prod_unitsSMul, HNNExtension.NormalWord.prod_injective, HNNExtension.NormalWord.prod_empty, HNNExtension.NormalWord.prod_smul_empty, HNNExtension.ReducedWord.exists_normalWord_prod_eq
toList 📖	CompOp	11 math math: HNNExtension.NormalWord.group_smul_toList, chain, empty_toList, HNNExtension.NormalWord.ext_iff, HNNExtension.NormalWord.group_smul_def, HNNExtension.NormalWord.empty_toList, HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq, HNNExtension.NormalWord.cons_toList, HNNExtension.NormalWord.ofGroup_toList, HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range, HNNExtension.ReducedWord.exists_normalWord_prod_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chain 📖	mathematical	—	Units Int.instMonoid toList	—	—
empty_head 📖	mathematical	—	head empty InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
empty_toList 📖	mathematical	—	toList empty Units Int.instMonoid	—	—

HNNExtension.NormalWord.TransversalPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	—	Subgroup.IsComplement SetLike.coe Subgroup Subgroup.instSetLike HNNExtension.toSubgroup set	—	—
nonempty 📖	mathematical	—	HNNExtension.NormalWord.TransversalPair	—	Subgroup.exists_isComplement_right

HNNExtension.ReducedWord

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_normalWord_prod_eq 📖	mathematical	—	HNNExtension.NormalWord.ReducedWord.prod HNNExtension.NormalWord.toReducedWord Units Int.instMonoid HNNExtension.NormalWord.ReducedWord.toList Subgroup SetLike.instMembership Subgroup.instSetLike HNNExtension.toSubgroup Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid HNNExtension.NormalWord.ReducedWord.head	—	List.isChain_nil instIsEmptyFalse SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass List.isChain_cons HNNExtension.NormalWord.prod_smul map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul neg_neg mul_mem_cancel_right Int.instCharZero SemigroupAction.mul_smul HNNExtension.NormalWord.of_smul_eq_smul HNNExtension.NormalWord.ReducedWord.chain HNNExtension.NormalWord.mem_set HNNExtension.NormalWord.group_smul_def HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul HNNExtension.NormalWord.unitsSMul.eq_1 HNNExtension.NormalWord.TransversalPair.compl mul_inv_rev HNNExtension.NormalWord.cons.congr_simp mul_assoc inv_mul_cancel_left inv_mul_cancel mul_one SubgroupClass.toInvMemClass map_mul MonoidHomClass.toMulHomClass LeftCancelSemigroup.toIsLeftCancelMul
map_fst_eq_and_of_prod_eq 📖	mathematical	HNNExtension.NormalWord.ReducedWord.prod	Units Int.instMonoid HNNExtension.NormalWord.ReducedWord.toList Subgroup SetLike.instMembership Subgroup.instSetLike HNNExtension.toSubgroup Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid HNNExtension.NormalWord.ReducedWord.head	—	HNNExtension.NormalWord.TransversalPair.nonempty exists_normalWord_prod_eq HNNExtension.NormalWord.prod_injective
toList_eq_nil_of_mem_of_range 📖	mathematical	HNNExtension Subgroup instGroupHNNExtension SetLike.instMembership Subgroup.instSetLike MonoidHom.range HNNExtension.of HNNExtension.NormalWord.ReducedWord.prod	HNNExtension.NormalWord.ReducedWord.toList Units Int.instMonoid	—	HNNExtension.NormalWord.ReducedWord.chain mul_one map_fst_eq_and_of_prod_eq

(root)

Definitions

Name	Category	Theorems
HNNExtension 📖	CompOp	21 math math: HNNExtension.NormalWord.prod_group_smul, HNNExtension.NormalWord.t_smul_eq_unitsSMul, HNNExtension.lift_of, HNNExtension.equiv_eq_conj, HNNExtension.NormalWord.prod_cons, HNNExtension.inv_t_mul_of, HNNExtension.NormalWord.prod_smul, HNNExtension.NormalWord.prod_unitsSMul, HNNExtension.NormalWord.prod_injective, HNNExtension.NormalWord.instFaithfulSMul_1, HNNExtension.of_mul_t, HNNExtension.of_mul_inv_t, HNNExtension.lift_t, HNNExtension.NormalWord.prod_empty, HNNExtension.t_mul_of, HNNExtension.hom_ext_iff, HNNExtension.of_injective, HNNExtension.NormalWord.of_smul_eq_smul, HNNExtension.equiv_symm_eq_conj, HNNExtension.NormalWord.prod_smul_empty, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul
instGroupHNNExtension 📖	CompOp	20 math math: HNNExtension.NormalWord.prod_group_smul, HNNExtension.NormalWord.t_smul_eq_unitsSMul, HNNExtension.lift_of, HNNExtension.equiv_eq_conj, HNNExtension.NormalWord.prod_cons, HNNExtension.inv_t_mul_of, HNNExtension.NormalWord.prod_smul, HNNExtension.NormalWord.prod_unitsSMul, HNNExtension.NormalWord.instFaithfulSMul_1, HNNExtension.of_mul_t, HNNExtension.of_mul_inv_t, HNNExtension.lift_t, HNNExtension.NormalWord.prod_empty, HNNExtension.t_mul_of, HNNExtension.hom_ext_iff, HNNExtension.of_injective, HNNExtension.NormalWord.of_smul_eq_smul, HNNExtension.equiv_symm_eq_conj, HNNExtension.NormalWord.prod_smul_empty, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul

---

← Back to Index