Commit 2023-09-14 10:14 1e1cdbfc

View on Github →

feat: HNN extensions and Britton's lemma (#6923)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/HNNExtension.lean

added def HNNExtension.NormalWord.Cancels

added def HNNExtension.NormalWord.ReducedWord.empty

added def HNNExtension.NormalWord.ReducedWord.prod

added structure HNNExtension.NormalWord.ReducedWord

added structure HNNExtension.NormalWord.TransversalPair

added def HNNExtension.NormalWord.cons

added def HNNExtension.NormalWord.consRecOn

added theorem HNNExtension.NormalWord.consRecOn_cons

added theorem HNNExtension.NormalWord.consRecOn_ofGroup

added def HNNExtension.NormalWord.empty

added theorem HNNExtension.NormalWord.ext

added theorem HNNExtension.NormalWord.group_smul_def

added theorem HNNExtension.NormalWord.group_smul_head

added theorem HNNExtension.NormalWord.group_smul_toList

added theorem HNNExtension.NormalWord.not_cancels_of_cons_hyp

added def HNNExtension.NormalWord.ofGroup

added theorem HNNExtension.NormalWord.of_smul_eq_smul

added theorem HNNExtension.NormalWord.prod_cons

added theorem HNNExtension.NormalWord.prod_empty

added theorem HNNExtension.NormalWord.prod_group_smul

added theorem HNNExtension.NormalWord.prod_injective

added theorem HNNExtension.NormalWord.prod_smul

added theorem HNNExtension.NormalWord.prod_smul_empty

added theorem HNNExtension.NormalWord.prod_unitsSMul

added theorem HNNExtension.NormalWord.smul_cons

added theorem HNNExtension.NormalWord.smul_ofGroup

added theorem HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul

added theorem HNNExtension.NormalWord.t_smul_eq_unitsSMul

added theorem HNNExtension.NormalWord.unitsSMulGroup_snd

added def HNNExtension.NormalWord.unitsSMulWithCancel

added theorem HNNExtension.NormalWord.unitsSMul_cancels_iff

added theorem HNNExtension.NormalWord.unitsSMul_neg

added theorem HNNExtension.NormalWord.unitsSMul_one_group_smul

added structure HNNExtension.NormalWord

added theorem HNNExtension.ReducedWord.exists_normalWord_prod_eq

added theorem HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq

added theorem HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range

added def HNNExtension.con

added theorem HNNExtension.equiv_eq_conj

added theorem HNNExtension.equiv_symm_eq_conj

added theorem HNNExtension.hom_ext

added theorem HNNExtension.induction_on

added theorem HNNExtension.inv_t_mul_of

added def HNNExtension.lift

added theorem HNNExtension.lift_of

added theorem HNNExtension.lift_t

added def HNNExtension.of

added theorem HNNExtension.of_injective

added theorem HNNExtension.of_mul_inv_t

added theorem HNNExtension.of_mul_t

added def HNNExtension.t

added theorem HNNExtension.t_mul_of

added def HNNExtension.toSubgroup

added def HNNExtension.toSubgroupEquiv

added theorem HNNExtension.toSubgroupEquiv_neg_apply

added theorem HNNExtension.toSubgroupEquiv_neg_one

added theorem HNNExtension.toSubgroupEquiv_one

added theorem HNNExtension.toSubgroup_neg_one

added theorem HNNExtension.toSubgroup_one

added def HNNExtension