Documentation

Mathlib.GroupTheory.FreeGroup.Basic

Free groups #

This file defines free groups over a type. Furthermore, it is shown that the free group construction is an instance of a monad. For the result that FreeGroup is the left adjoint to the forgetful functor from groups to types, see Algebra/Category/Group/Adjunctions.

Main definitions #

Main statements #

Implementation details #

First we introduce the one step reduction relation FreeGroup.Red.Step: w * x * x⁻¹ * v ~> w * v, its reflexive transitive closure FreeGroup.Red.trans and prove that its join is an equivalence relation. Then we introduce FreeGroup α as a quotient over FreeGroup.Red.Step.

For the additive version we introduce the same relation under a different name so that we can distinguish the quotient types more easily.

Tags #

free group, Newman's diamond lemma, Church-Rosser theorem

inductive FreeAddGroup.Red.Step {α : Type u} :
List (α × Bool)List (α × Bool)Prop

Reduction step for the additive free group relation: w + x + (-x) + v ~> w + v

Instances For
    inductive FreeGroup.Red.Step {α : Type u} :
    List (α × Bool)List (α × Bool)Prop

    Reduction step for the multiplicative free group relation: w * x * x⁻¹ * v ~> w * v

    Instances For
      def FreeAddGroup.Red {α : Type u} :
      List (α × Bool)List (α × Bool)Prop

      Reflexive-transitive closure of Red.Step

      Equations
      Instances For
        def FreeGroup.Red {α : Type u} :
        List (α × Bool)List (α × Bool)Prop

        Reflexive-transitive closure of Red.Step

        Equations
        Instances For
          theorem FreeAddGroup.Red.refl {α : Type u} {L : List (α × Bool)} :
          theorem FreeGroup.Red.refl {α : Type u} {L : List (α × Bool)} :
          theorem FreeAddGroup.Red.trans {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
          FreeAddGroup.Red L₁ L₂FreeAddGroup.Red L₂ L₃FreeAddGroup.Red L₁ L₃
          theorem FreeGroup.Red.trans {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
          FreeGroup.Red L₁ L₂FreeGroup.Red L₂ L₃FreeGroup.Red L₁ L₃
          abbrev FreeAddGroup.Red.Step.length.match_1 {α : Type u_1} (motive : (x x_1 : List (α × Bool)) → FreeAddGroup.Red.Step x x_1Prop) :
          ∀ (x x_1 : List (α × Bool)) (x_2 : FreeAddGroup.Red.Step x x_1), (∀ (L1 L2 : List (α × Bool)) (x : α) (b : Bool), motive (L1 ++ (x, b) :: (x, !b) :: L2) (L1 ++ L2) )motive x x_1 x_2
          Equations
          • =
          Instances For
            theorem FreeAddGroup.Red.Step.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
            FreeAddGroup.Red.Step L₁ L₂List.length L₂ + 2 = List.length L₁

            Predicate asserting that the word w₁ can be reduced to w₂ in one step, i.e. there are words w₃ w₄ and letter x such that w₁ = w₃ + x + (-x) + w₄ and w₂ = w₃w₄

            theorem FreeGroup.Red.Step.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
            FreeGroup.Red.Step L₁ L₂List.length L₂ + 2 = List.length L₁

            Predicate asserting that the word w₁ can be reduced to w₂ in one step, i.e. there are words w₃ w₄ and letter x such that w₁ = w₃xx⁻¹w₄ and w₂ = w₃w₄

            @[simp]
            theorem FreeAddGroup.Red.Step.not_rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α} {b : Bool} :
            FreeAddGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
            @[simp]
            theorem FreeGroup.Red.Step.not_rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α} {b : Bool} :
            FreeGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
            @[simp]
            theorem FreeAddGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
            FreeAddGroup.Red.Step ((x, b) :: (x, !b) :: L) L
            @[simp]
            theorem FreeGroup.Red.Step.cons_not {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
            FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L
            @[simp]
            theorem FreeAddGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
            FreeAddGroup.Red.Step ((x, !b) :: (x, b) :: L) L
            @[simp]
            theorem FreeGroup.Red.Step.cons_not_rev {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
            FreeGroup.Red.Step ((x, !b) :: (x, b) :: L) L
            abbrev FreeAddGroup.Red.Step.append_left.match_1 {α : Type u_1} (motive : List (α × Bool)(x x_1 : List (α × Bool)) → FreeAddGroup.Red.Step x x_1Prop) :
            ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : FreeAddGroup.Red.Step x_1 x_2), (∀ (x L₁ L₂ : List (α × Bool)) (x_4 : α) (b : Bool), motive x (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂) )motive x x_1 x_2 x_3
            Equations
            • =
            Instances For
              theorem FreeAddGroup.Red.Step.append_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
              FreeAddGroup.Red.Step L₂ L₃FreeAddGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
              theorem FreeGroup.Red.Step.append_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
              FreeGroup.Red.Step L₂ L₃FreeGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
              theorem FreeAddGroup.Red.Step.cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α × Bool} (H : FreeAddGroup.Red.Step L₁ L₂) :
              FreeAddGroup.Red.Step (x :: L₁) (x :: L₂)
              theorem FreeGroup.Red.Step.cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x : α × Bool} (H : FreeGroup.Red.Step L₁ L₂) :
              FreeGroup.Red.Step (x :: L₁) (x :: L₂)
              abbrev FreeAddGroup.Red.Step.append_right.match_1 {α : Type u_1} (motive : (x x_1 : List (α × Bool)) → List (α × Bool)FreeAddGroup.Red.Step x x_1Prop) :
              ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : FreeAddGroup.Red.Step x x_1), (∀ (x L₁ L₂ : List (α × Bool)) (x_4 : α) (b : Bool), motive (L₁ ++ (x_4, b) :: (x_4, !b) :: L₂) (L₁ ++ L₂) x )motive x x_1 x_2 x_3
              Equations
              • =
              Instances For
                theorem FreeAddGroup.Red.Step.append_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
                FreeAddGroup.Red.Step L₁ L₂FreeAddGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
                theorem FreeGroup.Red.Step.append_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
                FreeGroup.Red.Step L₁ L₂FreeGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
                theorem FreeAddGroup.Red.Step.cons_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {a : α} {b : Bool} :
                FreeAddGroup.Red.Step ((a, b) :: L₁) L₂ (∃ (L : List (α × Bool)), FreeAddGroup.Red.Step L₁ L L₂ = (a, b) :: L) L₁ = (a, !b) :: L₂
                theorem FreeGroup.Red.Step.cons_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {a : α} {b : Bool} :
                FreeGroup.Red.Step ((a, b) :: L₁) L₂ (∃ (L : List (α × Bool)), FreeGroup.Red.Step L₁ L L₂ = (a, b) :: L) L₁ = (a, !b) :: L₂
                abbrev FreeAddGroup.Red.not_step_singleton.match_1 {α : Type u_1} (motive : α × BoolProp) :
                ∀ (x : α × Bool), (∀ (a : α) (b : Bool), motive (a, b))motive x
                Equations
                • =
                Instances For
                  theorem FreeAddGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} :
                  theorem FreeGroup.Red.Step.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} :
                  FreeGroup.Red.Step (p :: L₁) (p :: L₂) FreeGroup.Red.Step L₁ L₂
                  abbrev FreeAddGroup.Red.Step.append_left_iff.match_1 {α : Type u_1} (motive : List (α × Bool)Prop) :
                  ∀ (x : List (α × Bool)), (Unitmotive [])(∀ (p : α × Bool) (l : List (α × Bool)), motive (p :: l))motive x
                  Equations
                  • =
                  Instances For
                    theorem FreeAddGroup.Red.Step.append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) :
                    theorem FreeGroup.Red.Step.append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) :
                    FreeGroup.Red.Step (L ++ L₁) (L ++ L₂) FreeGroup.Red.Step L₁ L₂
                    abbrev FreeAddGroup.Red.Step.diamond_aux.match_3 {α : Type u_1} (motive : (x x_1 x_2 x_3 : List (α × Bool)) → (x_4 : α) → (x_5 : Bool) → (x_6 : α) → (x_7 : Bool) → x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3Prop) :
                    ∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : α) (x_5 : Bool) (x_6 : α) (x_7 : Bool) (x_8 : x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3), (∀ (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x [] x_9 x_10 x_11 x_12 x_13 H)(∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [(x3, b3)] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x [(x3, b3)] x_9 x_10 x_11 x_12 x_13 H)(∀ (x3 : α) (b3 : Bool) (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [(x3, b3)] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [(x3, b3)] x [] x_9 x_10 x_11 x_12 x_13 H)(∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x3, b3) :: (x4, b4) :: tl ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive [] x ((x3, b3) :: (x4, b4) :: tl) x_9 x_10 x_11 x_12 x_13 H)(∀ (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : (x3, b3) :: (x4, b4) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive ((x3, b3) :: (x4, b4) :: tl) x [] x_9 x_10 x_11 x_12 x_13 H)(∀ (x3 : α) (b3 : Bool) (tl x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool) (H : (x3, b3) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x = (x4, b4) :: tl2 ++ (x_12, x_13) :: (x_12, !x_13) :: x_9), motive ((x3, b3) :: tl) x ((x4, b4) :: tl2) x_9 x_10 x_11 x_12 x_13 H)motive x x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8
                    Equations
                    • =
                    Instances For
                      theorem FreeAddGroup.Red.Step.diamond_aux {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} :
                      L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄L₁ ++ L₂ = L₃ ++ L₄ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (L₁ ++ L₂) L₅ FreeAddGroup.Red.Step (L₃ ++ L₄) L₅
                      abbrev FreeAddGroup.Red.Step.diamond_aux.match_1 {α : Type u_1} (tl : List (α × Bool)) :
                      ∀ (x tl2 x_1 : List (α × Bool)) (motive : (tl ++ x = tl2 ++ x_1 ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅)Prop) (x_2 : tl ++ x = tl2 ++ x_1 ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step (tl ++ x) L₅ FreeAddGroup.Red.Step (tl2 ++ x_1) L₅), (∀ (H3 : tl ++ x = tl2 ++ x_1), motive )(∀ (L₅ : List (α × Bool)) (H3 : FreeAddGroup.Red.Step (tl ++ x) L₅) (H4 : FreeAddGroup.Red.Step (tl2 ++ x_1) L₅), motive )motive x_2
                      Equations
                      • =
                      Instances For
                        abbrev FreeAddGroup.Red.Step.diamond_aux.match_2 {α : Type u_1} (x3 : α) (b3 : Bool) (tl : List (α × Bool)) :
                        ∀ (x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_1 : List (α × Bool)) (x_2 : α) (x_3 : Bool) (x_4 : α) (x_5 : Bool) (motive : (x3, b3) = (x4, b4) List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)Prop) (x_6 : (x3, b3) = (x4, b4) List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)), (∀ (H1 : (x3, b3) = (x4, b4)) (H2 : List.append tl ((x_2, x_3) :: (x_2, !x_3) :: x) = List.append tl2 ((x_4, x_5) :: (x_4, !x_5) :: x_1)), motive )motive x_6
                        Equations
                        • =
                        Instances For
                          theorem FreeGroup.Red.Step.diamond_aux {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} :
                          L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄L₁ ++ L₂ = L₃ ++ L₄ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step (L₁ ++ L₂) L₅ FreeGroup.Red.Step (L₃ ++ L₄) L₅
                          theorem FreeAddGroup.Red.Step.diamond {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} :
                          FreeAddGroup.Red.Step L₁ L₃FreeAddGroup.Red.Step L₂ L₄L₁ = L₂L₃ = L₄ ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step L₃ L₅ FreeAddGroup.Red.Step L₄ L₅
                          abbrev FreeAddGroup.Red.Step.diamond.match_1 {α : Type u_1} (motive : (x x_1 x_2 x_3 : List (α × Bool)) → FreeAddGroup.Red.Step x x_2FreeAddGroup.Red.Step x_1 x_3x = x_1Prop) :
                          ∀ (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : FreeAddGroup.Red.Step x x_2) (x_5 : FreeAddGroup.Red.Step x_1 x_3) (x_6 : x = x_1), (∀ (L₁ L₂ : List (α × Bool)) (x : α) (b : Bool) (L₁_1 L₂_1 : List (α × Bool)) (x_7 : α) (b_1 : Bool) (H : L₁ ++ (x, b) :: (x, !b) :: L₂ = L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1), motive (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁_1 ++ (x_7, b_1) :: (x_7, !b_1) :: L₂_1) (L₁ ++ L₂) (L₁_1 ++ L₂_1) H)motive x x_1 x_2 x_3 x_4 x_5 x_6
                          Equations
                          • =
                          Instances For
                            theorem FreeGroup.Red.Step.diamond {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} :
                            FreeGroup.Red.Step L₁ L₃FreeGroup.Red.Step L₂ L₄L₁ = L₂L₃ = L₄ ∃ (L₅ : List (α × Bool)), FreeGroup.Red.Step L₃ L₅ FreeGroup.Red.Step L₄ L₅
                            theorem FreeAddGroup.Red.Step.to_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                            FreeAddGroup.Red.Step L₁ L₂FreeAddGroup.Red L₁ L₂
                            theorem FreeGroup.Red.Step.to_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                            FreeGroup.Red.Step L₁ L₂FreeGroup.Red L₁ L₂
                            theorem FreeAddGroup.Red.church_rosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
                            FreeAddGroup.Red L₁ L₂FreeAddGroup.Red L₁ L₃Relation.Join FreeAddGroup.Red L₂ L₃

                            Church-Rosser theorem for word reduction: If w1 w2 w3 are words such that w1 reduces to w2 and w3 respectively, then there is a word w4 such that w2 and w3 reduce to w4 respectively. This is also known as Newman's diamond lemma.

                            abbrev FreeAddGroup.Red.church_rosser.match_1 {α : Type u_1} (a : List (α × Bool)) (motive : (b c : List (α × Bool)) → (b = c ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ FreeAddGroup.Red.Step c L₅)FreeAddGroup.Red.Step a bFreeAddGroup.Red.Step a cProp) :
                            ∀ (b c : List (α × Bool)) (x : b = c ∃ (L₅ : List (α × Bool)), FreeAddGroup.Red.Step b L₅ FreeAddGroup.Red.Step c L₅) (hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c), (∀ (b : List (α × Bool)) (hab hac : FreeAddGroup.Red.Step a b), motive b b hab hac)(∀ (b c d : List (α × Bool)) (hbd : FreeAddGroup.Red.Step b d) (hcd : FreeAddGroup.Red.Step c d) (hab : FreeAddGroup.Red.Step a b) (hac : FreeAddGroup.Red.Step a c), motive b c hab hac)motive b c x hab hac
                            Equations
                            • =
                            Instances For
                              theorem FreeGroup.Red.church_rosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} :
                              FreeGroup.Red L₁ L₂FreeGroup.Red L₁ L₃Relation.Join FreeGroup.Red L₂ L₃

                              Church-Rosser theorem for word reduction: If w1 w2 w3 are words such that w1 reduces to w2 and w3 respectively, then there is a word w4 such that w2 and w3 reduce to w4 respectively. This is also known as Newman's diamond lemma.

                              theorem FreeAddGroup.Red.cons_cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} :
                              FreeAddGroup.Red L₁ L₂FreeAddGroup.Red (p :: L₁) (p :: L₂)
                              theorem FreeGroup.Red.cons_cons {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {p : α × Bool} :
                              FreeGroup.Red L₁ L₂FreeGroup.Red (p :: L₁) (p :: L₂)
                              theorem FreeAddGroup.Red.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (p : α × Bool) :
                              FreeAddGroup.Red (p :: L₁) (p :: L₂) FreeAddGroup.Red L₁ L₂
                              theorem FreeGroup.Red.cons_cons_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (p : α × Bool) :
                              FreeGroup.Red (p :: L₁) (p :: L₂) FreeGroup.Red L₁ L₂
                              theorem FreeAddGroup.Red.append_append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) :
                              FreeAddGroup.Red (L ++ L₁) (L ++ L₂) FreeAddGroup.Red L₁ L₂
                              theorem FreeGroup.Red.append_append_left_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (L : List (α × Bool)) :
                              FreeGroup.Red (L ++ L₁) (L ++ L₂) FreeGroup.Red L₁ L₂
                              theorem FreeAddGroup.Red.append_append {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} (h₁ : FreeAddGroup.Red L₁ L₃) (h₂ : FreeAddGroup.Red L₂ L₄) :
                              FreeAddGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
                              theorem FreeGroup.Red.append_append {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {L₄ : List (α × Bool)} (h₁ : FreeGroup.Red L₁ L₃) (h₂ : FreeGroup.Red L₂ L₄) :
                              FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
                              abbrev FreeAddGroup.Red.to_append_iff.match_1 {α : Type u_1} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (motive : (∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ FreeAddGroup.Red L₃ L₁ FreeAddGroup.Red L₄ L₂)Prop) :
                              ∀ (x : ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ FreeAddGroup.Red L₃ L₁ FreeAddGroup.Red L₄ L₂), (∀ (L₃ L₄ : List (α × Bool)) (Eq : L = L₃ ++ L₄) (h₃ : FreeAddGroup.Red L₃ L₁) (h₄ : FreeAddGroup.Red L₄ L₂), motive )motive x
                              Equations
                              • =
                              Instances For
                                theorem FreeAddGroup.Red.to_append_iff {α : Type u} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                FreeAddGroup.Red L (L₁ ++ L₂) ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ FreeAddGroup.Red L₃ L₁ FreeAddGroup.Red L₄ L₂
                                theorem FreeGroup.Red.to_append_iff {α : Type u} {L : List (α × Bool)} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                FreeGroup.Red L (L₁ ++ L₂) ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ FreeGroup.Red L₃ L₁ FreeGroup.Red L₄ L₂
                                theorem FreeAddGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} :

                                The empty word [] only reduces to itself.

                                theorem FreeGroup.Red.nil_iff {α : Type u} {L : List (α × Bool)} :
                                FreeGroup.Red [] L L = []

                                The empty word [] only reduces to itself.

                                theorem FreeAddGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} :
                                FreeAddGroup.Red [x] L₁ L₁ = [x]

                                A letter only reduces to itself.

                                theorem FreeGroup.Red.singleton_iff {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool} :
                                FreeGroup.Red [x] L₁ L₁ = [x]

                                A letter only reduces to itself.

                                theorem FreeAddGroup.Red.cons_nil_iff_singleton {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
                                FreeAddGroup.Red ((x, b) :: L) [] FreeAddGroup.Red L [(x, !b)]

                                If x is a letter and w is a word such that x + w reduces to the empty word, then w reduces to -x.

                                abbrev FreeAddGroup.Red.cons_nil_iff_singleton.match_1 {α : Type u_1} {L : List (α × Bool)} {x : α} {b : Bool} (motive : Relation.Join FreeAddGroup.Red [(x, !b)] LProp) :
                                ∀ (x_1 : Relation.Join FreeAddGroup.Red [(x, !b)] L), (∀ (L' : List (α × Bool)) (h₁ : FreeAddGroup.Red [(x, !b)] L') (h₂ : FreeAddGroup.Red L L'), motive )motive x_1
                                Equations
                                • =
                                Instances For
                                  theorem FreeGroup.Red.cons_nil_iff_singleton {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool} :
                                  FreeGroup.Red ((x, b) :: L) [] FreeGroup.Red L [(x, !b)]

                                  If x is a letter and w is a word such that xw reduces to the empty word, then w reduces to x⁻¹

                                  theorem FreeAddGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) (x2, b2)) :
                                  FreeAddGroup.Red [(x1, !b1), (x2, b2)] L L = [(x1, !b1), (x2, b2)]
                                  theorem FreeGroup.Red.red_iff_irreducible {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (h : (x1, b1) (x2, b2)) :
                                  FreeGroup.Red [(x1, !b1), (x2, b2)] L L = [(x1, !b1), (x2, b2)]
                                  theorem FreeAddGroup.Red.neg_of_red_of_ne {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (H1 : (x1, b1) (x2, b2)) (H2 : FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
                                  FreeAddGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

                                  If x and y are distinct letters and w₁ w₂ are words such that x + w₁ reduces to y + w₂, then w₁ reduces to -x + y + w₂.

                                  theorem FreeGroup.Red.inv_of_red_of_ne {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool} (H1 : (x1, b1) (x2, b2)) (H2 : FreeGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
                                  FreeGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

                                  If x and y are distinct letters and w₁ w₂ are words such that xw₁ reduces to yw₂, then w₁ reduces to x⁻¹yw₂.

                                  theorem FreeAddGroup.Red.Step.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (H : FreeAddGroup.Red.Step L₁ L₂) :
                                  List.Sublist L₂ L₁
                                  theorem FreeGroup.Red.Step.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (H : FreeGroup.Red.Step L₁ L₂) :
                                  List.Sublist L₂ L₁
                                  theorem FreeAddGroup.Red.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  FreeAddGroup.Red L₁ L₂List.Sublist L₂ L₁

                                  If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

                                  theorem FreeGroup.Red.sublist {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  FreeGroup.Red L₁ L₂List.Sublist L₂ L₁

                                  If w₁ w₂ are words such that w₁ reduces to w₂, then w₂ is a sublist of w₁.

                                  theorem FreeAddGroup.Red.length_le {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :
                                  theorem FreeGroup.Red.length_le {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :
                                  theorem FreeAddGroup.Red.sizeof_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  FreeAddGroup.Red.Step L₁ L₂sizeOf L₂ < sizeOf L₁
                                  theorem FreeGroup.Red.sizeof_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  FreeGroup.Red.Step L₁ L₂sizeOf L₂ < sizeOf L₁
                                  theorem FreeAddGroup.Red.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :
                                  ∃ (n : ), List.length L₁ = List.length L₂ + 2 * n
                                  theorem FreeGroup.Red.length {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :
                                  ∃ (n : ), List.length L₁ = List.length L₂ + 2 * n
                                  theorem FreeAddGroup.Red.antisymm {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h₁₂ : FreeAddGroup.Red L₁ L₂) (h₂₁ : FreeAddGroup.Red L₂ L₁) :
                                  L₁ = L₂
                                  theorem FreeGroup.Red.antisymm {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h₁₂ : FreeGroup.Red L₁ L₂) (h₂₁ : FreeGroup.Red L₂ L₁) :
                                  L₁ = L₂
                                  theorem FreeAddGroup.join_red_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red.Step L₁ L₂) :
                                  Relation.Join FreeAddGroup.Red L₁ L₂
                                  theorem FreeGroup.join_red_of_step {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) :
                                  Relation.Join FreeGroup.Red L₁ L₂
                                  theorem FreeAddGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  EqvGen FreeAddGroup.Red.Step L₁ L₂ Relation.Join FreeAddGroup.Red L₁ L₂
                                  theorem FreeGroup.eqvGen_step_iff_join_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                  EqvGen FreeGroup.Red.Step L₁ L₂ Relation.Join FreeGroup.Red L₁ L₂
                                  def FreeAddGroup (α : Type u) :

                                  The free additive group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.

                                  Equations
                                  Instances For
                                    def FreeGroup (α : Type u) :

                                    The free group over a type, i.e. the words formed by the elements of the type and their formal inverses, quotient by one step reduction.

                                    Equations
                                    Instances For
                                      def FreeAddGroup.mk {α : Type u} (L : List (α × Bool)) :

                                      The canonical map from list (α × bool) to the free additive group on α.

                                      Equations
                                      Instances For
                                        def FreeGroup.mk {α : Type u} (L : List (α × Bool)) :

                                        The canonical map from List (α × Bool) to the free group on α.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem FreeAddGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} :
                                          Quot.mk FreeAddGroup.Red.Step L = FreeAddGroup.mk L
                                          @[simp]
                                          theorem FreeGroup.quot_mk_eq_mk {α : Type u} {L : List (α × Bool)} :
                                          Quot.mk FreeGroup.Red.Step L = FreeGroup.mk L
                                          @[simp]
                                          theorem FreeAddGroup.quot_lift_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂f L₁ = f L₂) :
                                          @[simp]
                                          theorem FreeGroup.quot_lift_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂f L₁ = f L₂) :
                                          @[simp]
                                          theorem FreeAddGroup.quot_liftOn_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeAddGroup.Red.Step L₁ L₂f L₁ = f L₂) :
                                          @[simp]
                                          theorem FreeGroup.quot_liftOn_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)β) (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂f L₁ = f L₂) :
                                          @[simp]
                                          theorem FreeAddGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)List (β × Bool)) (H : (FreeAddGroup.Red.Step FreeAddGroup.Red.Step) f f) :
                                          @[simp]
                                          theorem FreeGroup.quot_map_mk {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool)List (β × Bool)) (H : (FreeGroup.Red.Step FreeGroup.Red.Step) f f) :
                                          Equations
                                          Equations
                                          Equations
                                          • FreeAddGroup.instInhabitedFreeAddGroup = { default := 0 }
                                          Equations
                                          • FreeGroup.instInhabitedFreeGroup = { default := 1 }
                                          Equations
                                          • FreeAddGroup.instUniqueFreeAddGroup = id inferInstance
                                          Equations
                                          • FreeGroup.instUniqueFreeGroup = id inferInstance
                                          theorem FreeAddGroup.instAddFreeAddGroup.proof_1 {α : Type u_1} (L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (_L₃ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₂ _L₃) :
                                          Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₂) = Quot.mk FreeAddGroup.Red.Step (L₁ ++ _L₃)
                                          theorem FreeAddGroup.instAddFreeAddGroup.proof_2 {α : Type u_1} (y : FreeAddGroup α) (_L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₁ _L₂) :
                                          (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ) _L₁ = (fun (L₁ : List (α × Bool)) => Quot.liftOn y (fun (L₂ : List (α × Bool)) => FreeAddGroup.mk (L₁ ++ L₂)) ) _L₂
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          @[simp]
                                          theorem FreeAddGroup.add_mk {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                          @[simp]
                                          theorem FreeGroup.mul_mk {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                          FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)
                                          def FreeAddGroup.negRev {α : Type u} (w : List (α × Bool)) :
                                          List (α × Bool)

                                          Transform a word representing a free group element into a word representing its negative.

                                          Equations
                                          Instances For
                                            def FreeGroup.invRev {α : Type u} (w : List (α × Bool)) :
                                            List (α × Bool)

                                            Transform a word representing a free group element into a word representing its inverse.

                                            Equations
                                            Instances For
                                              @[simp]
                                              @[simp]
                                              theorem FreeGroup.invRev_length {α : Type u} {L₁ : List (α × Bool)} :
                                              @[simp]
                                              @[simp]
                                              theorem FreeGroup.invRev_invRev {α : Type u} {L₁ : List (α × Bool)} :
                                              @[simp]
                                              theorem FreeAddGroup.negRev_involutive {α : Type u} :
                                              Function.Involutive FreeAddGroup.negRev
                                              theorem FreeAddGroup.negRev_injective {α : Type u} :
                                              Function.Injective FreeAddGroup.negRev
                                              theorem FreeGroup.invRev_injective {α : Type u} :
                                              Function.Injective FreeGroup.invRev
                                              theorem FreeAddGroup.negRev_surjective {α : Type u} :
                                              Function.Surjective FreeAddGroup.negRev
                                              theorem FreeAddGroup.negRev_bijective {α : Type u} :
                                              Function.Bijective FreeAddGroup.negRev
                                              theorem FreeGroup.invRev_bijective {α : Type u} :
                                              Function.Bijective FreeGroup.invRev
                                              Equations
                                              • FreeAddGroup.instNegFreeAddGroup = { neg := Quot.map FreeAddGroup.negRev }
                                              Equations
                                              • FreeGroup.instInvFreeGroup = { inv := Quot.map FreeGroup.invRev }
                                              theorem FreeGroup.Red.Step.invRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red.Step L₁ L₂) :
                                              theorem FreeAddGroup.Red.negRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeAddGroup.Red L₁ L₂) :
                                              theorem FreeGroup.Red.invRev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (h : FreeGroup.Red L₁ L₂) :
                                              @[simp]
                                              @[simp]
                                              @[simp]
                                              theorem FreeGroup.red_invRev_iff {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_4 {α : Type u_1} :
                                              ∀ (x : FreeAddGroup α), nsmulRec 0 x = nsmulRec 0 x
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_1 {α : Type u_1} :
                                              ∀ (a b c : FreeAddGroup α), a + b + c = a + (b + c)
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_6 {α : Type u_1} :
                                              ∀ (a b : FreeAddGroup α), a - b = a - b
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_8 {α : Type u_1} :
                                              ∀ (n : ) (a : FreeAddGroup α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_7 {α : Type u_1} :
                                              ∀ (a : FreeAddGroup α), zsmulRec 0 a = zsmulRec 0 a
                                              Equations
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_5 {α : Type u_1} :
                                              ∀ (n : ) (x : FreeAddGroup α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
                                              theorem FreeAddGroup.instAddGroupFreeAddGroup.proof_9 {α : Type u_1} :
                                              ∀ (n : ) (a : FreeAddGroup α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
                                              Equations
                                              def FreeAddGroup.of {α : Type u} (x : α) :

                                              of is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element.

                                              Equations
                                              Instances For
                                                def FreeGroup.of {α : Type u} (x : α) :

                                                of is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element.

                                                Equations
                                                Instances For
                                                  theorem FreeAddGroup.Red.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                                  FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂ Relation.Join FreeAddGroup.Red L₁ L₂
                                                  theorem FreeGroup.Red.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} :
                                                  FreeGroup.mk L₁ = FreeGroup.mk L₂ Relation.Join FreeGroup.Red L₁ L₂
                                                  theorem FreeAddGroup.of_injective {α : Type u} :
                                                  Function.Injective FreeAddGroup.of

                                                  The canonical map from the type to the additive free group is an injection.

                                                  abbrev FreeAddGroup.of_injective.match_1 {α : Type u_1} :
                                                  ∀ (x x_1 : α) (motive : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)]Prop) (x_2 : Relation.Join FreeAddGroup.Red [(x, true)] [(x_1, true)]), (∀ (L₁ : List (α × Bool)) (hx : FreeAddGroup.Red [(x, true)] L₁) (hy : FreeAddGroup.Red [(x_1, true)] L₁), motive )motive x_2
                                                  Equations
                                                  • =
                                                  Instances For
                                                    theorem FreeGroup.of_injective {α : Type u} :
                                                    Function.Injective FreeGroup.of

                                                    The canonical map from the type to the free group is an injection.

                                                    def FreeAddGroup.Lift.aux {α : Type u} {β : Type v} [AddGroup β] (f : αβ) :
                                                    List (α × Bool)β

                                                    Given f : α → β with β an additive group, the canonical map list (α × bool) → β

                                                    Equations
                                                    Instances For
                                                      def FreeGroup.Lift.aux {α : Type u} {β : Type v} [Group β] (f : αβ) :
                                                      List (α × Bool)β

                                                      Given f : α → β with β a group, the canonical map List (α × Bool) → β

                                                      Equations
                                                      Instances For
                                                        theorem FreeAddGroup.Red.Step.lift {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {β : Type v} [AddGroup β] {f : αβ} (H : FreeAddGroup.Red.Step L₁ L₂) :
                                                        theorem FreeGroup.Red.Step.lift {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {β : Type v} [Group β] {f : αβ} (H : FreeGroup.Red.Step L₁ L₂) :
                                                        theorem FreeAddGroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : αβ) :
                                                        theorem FreeAddGroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [AddGroup β] (f : αβ) :
                                                        (0 + fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)) = fun (x : α) => (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) (x, true)
                                                        def FreeAddGroup.lift {α : Type u} {β : Type v} [AddGroup β] :
                                                        (αβ) (FreeAddGroup α →+ β)

                                                        If β is an additive group, then any function from α to β extends uniquely to an additive group homomorphism from the free additive group over α to β

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem FreeAddGroup.lift.proof_3 {α : Type u_2} {β : Type u_1} [AddGroup β] (g : FreeAddGroup α →+ β) :
                                                          (fun (f : αβ) => AddMonoidHom.mk' (Quot.lift (FreeAddGroup.Lift.aux f) ) ) ((fun (g : FreeAddGroup α →+ β) => g FreeAddGroup.of) g) = g
                                                          @[simp]
                                                          theorem FreeGroup.lift_symm_apply {α : Type u} {β : Type v} [Group β] (g : FreeGroup α →* β) :
                                                          ∀ (a : α), FreeGroup.lift.symm g a = (g FreeGroup.of) a
                                                          @[simp]
                                                          theorem FreeAddGroup.lift_symm_apply {α : Type u} {β : Type v} [AddGroup β] (g : FreeAddGroup α →+ β) :
                                                          ∀ (a : α), FreeAddGroup.lift.symm g a = (g FreeAddGroup.of) a
                                                          def FreeGroup.lift {α : Type u} {β : Type v} [Group β] :
                                                          (αβ) (FreeGroup α →* β)

                                                          If β is a group, then any function from α to β extends uniquely to a group homomorphism from the free group over α to β

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem FreeAddGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [AddGroup β] {f : αβ} :
                                                            (FreeAddGroup.lift f) (FreeAddGroup.mk L) = List.sum (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else -f x.1) L)
                                                            @[simp]
                                                            theorem FreeGroup.lift.mk {α : Type u} {L : List (α × Bool)} {β : Type v} [Group β] {f : αβ} :
                                                            (FreeGroup.lift f) (FreeGroup.mk L) = List.prod (List.map (fun (x : α × Bool) => bif x.2 then f x.1 else (f x.1)⁻¹) L)
                                                            @[simp]
                                                            theorem FreeAddGroup.lift.of {α : Type u} {β : Type v} [AddGroup β] {f : αβ} {x : α} :
                                                            (FreeAddGroup.lift f) (FreeAddGroup.of x) = f x
                                                            @[simp]
                                                            theorem FreeGroup.lift.of {α : Type u} {β : Type v} [Group β] {f : αβ} {x : α} :
                                                            (FreeGroup.lift f) (FreeGroup.of x) = f x
                                                            theorem FreeAddGroup.lift.unique {α : Type u} {β : Type v} [AddGroup β] {f : αβ} (g : FreeAddGroup α →+ β) (hg : ∀ (x : α), g (FreeAddGroup.of x) = f x) {x : FreeAddGroup α} :
                                                            g x = (FreeAddGroup.lift f) x
                                                            theorem FreeGroup.lift.unique {α : Type u} {β : Type v} [Group β] {f : αβ} (g : FreeGroup α →* β) (hg : ∀ (x : α), g (FreeGroup.of x) = f x) {x : FreeGroup α} :
                                                            g x = (FreeGroup.lift f) x
                                                            theorem FreeAddGroup.ext_hom {α : Type u} {G : Type u_1} [AddGroup G] (f : FreeAddGroup α →+ G) (g : FreeAddGroup α →+ G) (h : ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)) :
                                                            f = g

                                                            Two homomorphisms out of a free additive group are equal if they are equal on generators. See note [partially-applied ext lemmas].

                                                            theorem FreeGroup.ext_hom {α : Type u} {G : Type u_1} [Group G] (f : FreeGroup α →* G) (g : FreeGroup α →* G) (h : ∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)) :
                                                            f = g

                                                            Two homomorphisms out of a free group are equal if they are equal on generators.

                                                            See note [partially-applied ext lemmas].

                                                            theorem FreeAddGroup.lift_of_eq_id (α : Type u_1) :
                                                            FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)
                                                            theorem FreeGroup.lift_of_eq_id (α : Type u_1) :
                                                            FreeGroup.lift FreeGroup.of = MonoidHom.id (FreeGroup α)
                                                            theorem FreeAddGroup.lift.of_eq {α : Type u} (x : FreeAddGroup α) :
                                                            (FreeAddGroup.lift FreeAddGroup.of) x = x
                                                            theorem FreeGroup.lift.of_eq {α : Type u} (x : FreeGroup α) :
                                                            (FreeGroup.lift FreeGroup.of) x = x
                                                            theorem FreeAddGroup.lift.range_le {α : Type u} {β : Type v} [AddGroup β] {f : αβ} {s : AddSubgroup β} (H : Set.range f s) :
                                                            AddMonoidHom.range (FreeAddGroup.lift f) s
                                                            theorem FreeGroup.lift.range_le {α : Type u} {β : Type v} [Group β] {f : αβ} {s : Subgroup β} (H : Set.range f s) :
                                                            MonoidHom.range (FreeGroup.lift f) s
                                                            theorem FreeAddGroup.lift.range_eq_closure {α : Type u} {β : Type v} [AddGroup β] {f : αβ} :
                                                            theorem FreeGroup.lift.range_eq_closure {α : Type u} {β : Type v} [Group β] {f : αβ} :
                                                            @[simp]
                                                            @[simp]
                                                            theorem FreeGroup.closure_range_of (α : Type u_1) :

                                                            The generators of FreeGroup α generate FreeGroup α. That is, the subgroup closure of the set of generators equals .

                                                            def FreeAddGroup.map {α : Type u} {β : Type v} (f : αβ) :

                                                            Any function from α to β extends uniquely to an additive group homomorphism from the additive free group over α to the additive free group over β.

                                                            Equations
                                                            Instances For
                                                              theorem FreeAddGroup.map.proof_2 {α : Type u_1} {β : Type u_2} (f : αβ) :
                                                              ∀ (a b : FreeAddGroup α), Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) (a + b) = Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) a + Quot.map (List.map fun (x : α × Bool) => (f x.1, x.2)) b
                                                              theorem FreeAddGroup.map.proof_1 {α : Type u_1} {β : Type u_2} (f : αβ) (L₁ : List (α × Bool)) (L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step L₁ L₂) :
                                                              FreeAddGroup.Red.Step (List.map (fun (x : α × Bool) => (f x.1, x.2)) L₁) (List.map (fun (x : α × Bool) => (f x.1, x.2)) L₂)
                                                              def FreeGroup.map {α : Type u} {β : Type v} (f : αβ) :

                                                              Any function from α to β extends uniquely to a group homomorphism from the free group over α to the free group over β.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem FreeAddGroup.map.mk {α : Type u} {L : List (α × Bool)} {β : Type v} {f : αβ} :
                                                                (FreeAddGroup.map f) (FreeAddGroup.mk L) = FreeAddGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)
                                                                @[simp]
                                                                theorem FreeGroup.map.mk {α : Type u} {L : List (α × Bool)} {β : Type v} {f : αβ} :
                                                                (FreeGroup.map f) (FreeGroup.mk L) = FreeGroup.mk (List.map (fun (x : α × Bool) => (f x.1, x.2)) L)
                                                                @[simp]
                                                                theorem FreeAddGroup.map.id {α : Type u} (x : FreeAddGroup α) :
                                                                @[simp]
                                                                theorem FreeGroup.map.id {α : Type u} (x : FreeGroup α) :
                                                                (FreeGroup.map id) x = x
                                                                @[simp]
                                                                theorem FreeAddGroup.map.id' {α : Type u} (x : FreeAddGroup α) :
                                                                (FreeAddGroup.map fun (z : α) => z) x = x
                                                                @[simp]
                                                                theorem FreeGroup.map.id' {α : Type u} (x : FreeGroup α) :
                                                                (FreeGroup.map fun (z : α) => z) x = x
                                                                theorem FreeAddGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (x : FreeAddGroup α) :
                                                                theorem FreeGroup.map.comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (x : FreeGroup α) :
                                                                @[simp]
                                                                theorem FreeAddGroup.map.of {α : Type u} {β : Type v} {f : αβ} {x : α} :
                                                                @[simp]
                                                                theorem FreeGroup.map.of {α : Type u} {β : Type v} {f : αβ} {x : α} :
                                                                theorem FreeAddGroup.map.unique {α : Type u} {β : Type v} {f : αβ} (g : FreeAddGroup α →+ FreeAddGroup β) (hg : ∀ (x : α), g (FreeAddGroup.of x) = FreeAddGroup.of (f x)) {x : FreeAddGroup α} :
                                                                theorem FreeGroup.map.unique {α : Type u} {β : Type v} {f : αβ} (g : FreeGroup α →* FreeGroup β) (hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)) {x : FreeGroup α} :
                                                                g x = (FreeGroup.map f) x
                                                                theorem FreeAddGroup.map_eq_lift {α : Type u} {β : Type v} {f : αβ} {x : FreeAddGroup α} :
                                                                (FreeAddGroup.map f) x = (FreeAddGroup.lift (FreeAddGroup.of f)) x
                                                                theorem FreeGroup.map_eq_lift {α : Type u} {β : Type v} {f : αβ} {x : FreeGroup α} :
                                                                (FreeGroup.map f) x = (FreeGroup.lift (FreeGroup.of f)) x
                                                                theorem FreeAddGroup.freeAddGroupCongr.proof_2 {α : Type u_2} {β : Type u_1} (e : α β) (x : FreeAddGroup β) :
                                                                (FreeAddGroup.map e) ((FreeAddGroup.map e.symm) x) = x
                                                                def FreeAddGroup.freeAddGroupCongr {α : Type u_1} {β : Type u_2} (e : α β) :

                                                                Equivalent types give rise to additively equivalent additive free groups.

                                                                Equations
                                                                Instances For
                                                                  theorem FreeAddGroup.freeAddGroupCongr.proof_3 {α : Type u_1} {β : Type u_2} (e : α β) (a : FreeAddGroup α) (b : FreeAddGroup α) :
                                                                  (FreeAddGroup.map e) (a + b) = (FreeAddGroup.map e) a + (FreeAddGroup.map e) b
                                                                  theorem FreeAddGroup.freeAddGroupCongr.proof_1 {α : Type u_1} {β : Type u_2} (e : α β) (x : FreeAddGroup α) :
                                                                  (FreeAddGroup.map e.symm) ((FreeAddGroup.map e) x) = x
                                                                  @[simp]
                                                                  theorem FreeGroup.freeGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) (a : FreeGroup α) :
                                                                  @[simp]
                                                                  theorem FreeAddGroup.freeAddGroupCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) (a : FreeAddGroup α) :
                                                                  def FreeGroup.freeGroupCongr {α : Type u_1} {β : Type u_2} (e : α β) :

                                                                  Equivalent types give rise to multiplicatively equivalent free groups.

                                                                  The converse can be found in GroupTheory.FreeAbelianGroupFinsupp, as Equiv.of_freeGroupEquiv

                                                                  Equations
                                                                  Instances For
                                                                    theorem FreeGroup.freeGroupCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :

                                                                    If α is an additive group, then any function from α to α extends uniquely to an additive homomorphism from the additive free group over α to α.

                                                                    Equations
                                                                    • FreeAddGroup.sum = FreeAddGroup.lift id
                                                                    Instances For
                                                                      def FreeGroup.prod {α : Type u} [Group α] :

                                                                      If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the multiplicative version of FreeGroup.sum.

                                                                      Equations
                                                                      • FreeGroup.prod = FreeGroup.lift id
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem FreeAddGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] :
                                                                        FreeAddGroup.sum (FreeAddGroup.mk L) = List.sum (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L)
                                                                        @[simp]
                                                                        theorem FreeGroup.prod_mk {α : Type u} {L : List (α × Bool)} [Group α] :
                                                                        FreeGroup.prod (FreeGroup.mk L) = List.prod (List.map (fun (x : α × Bool) => bif x.2 then x.1 else x.1⁻¹) L)
                                                                        @[simp]
                                                                        theorem FreeAddGroup.sum.of {α : Type u} [AddGroup α] {x : α} :
                                                                        FreeAddGroup.sum (FreeAddGroup.of x) = x
                                                                        @[simp]
                                                                        theorem FreeGroup.prod.of {α : Type u} [Group α] {x : α} :
                                                                        FreeGroup.prod (FreeGroup.of x) = x
                                                                        theorem FreeAddGroup.sum.unique {α : Type u} [AddGroup α] (g : FreeAddGroup α →+ α) (hg : ∀ (x : α), g (FreeAddGroup.of x) = x) {x : FreeAddGroup α} :
                                                                        g x = FreeAddGroup.sum x
                                                                        theorem FreeGroup.prod.unique {α : Type u} [Group α] (g : FreeGroup α →* α) (hg : ∀ (x : α), g (FreeGroup.of x) = x) {x : FreeGroup α} :
                                                                        g x = FreeGroup.prod x
                                                                        theorem FreeAddGroup.lift_eq_sum_map {α : Type u} {β : Type v} [AddGroup β] {f : αβ} {x : FreeAddGroup α} :
                                                                        (FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)
                                                                        theorem FreeGroup.lift_eq_prod_map {α : Type u} {β : Type v} [Group β] {f : αβ} {x : FreeGroup α} :
                                                                        (FreeGroup.lift f) x = FreeGroup.prod ((FreeGroup.map f) x)
                                                                        def FreeGroup.sum {α : Type u} [AddGroup α] (x : FreeGroup α) :
                                                                        α

                                                                        If α is a group, then any function from α to α extends uniquely to a homomorphism from the free group over α to α. This is the additive version of prod.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem FreeGroup.sum_mk {α : Type u} {L : List (α × Bool)} [AddGroup α] :
                                                                          FreeGroup.sum (FreeGroup.mk L) = List.sum (List.map (fun (x : α × Bool) => bif x.2 then x.1 else -x.1) L)
                                                                          @[simp]
                                                                          theorem FreeGroup.sum.of {α : Type u} [AddGroup α] {x : α} :
                                                                          @[simp]
                                                                          @[simp]
                                                                          theorem FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_2 :
                                                                          ∀ (x : Unit), (fun (x : FreeAddGroup Empty) => ()) ((fun (x : Unit) => 0) x) = x

                                                                          The bijection between the additive free group on the empty type, and a type with one element.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            theorem FreeAddGroup.freeAddGroupEmptyEquivAddUnit.proof_1 :
                                                                            ∀ (x : FreeAddGroup Empty), (fun (x : Unit) => 0) ((fun (x : FreeAddGroup Empty) => ()) x) = x
                                                                            abbrev FreeAddGroup.freeAddGroupEmptyEquivAddUnit.match_1 (motive : UnitProp) :
                                                                            ∀ (x : Unit), (Unitmotive PUnit.unit)motive x
                                                                            Equations
                                                                            • =
                                                                            Instances For

                                                                              The bijection between the free group on the empty type, and a type with one element.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                The bijection between the free group on a singleton, and the integers.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  theorem FreeAddGroup.induction_on {α : Type u} {C : FreeAddGroup αProp} (z : FreeAddGroup α) (C1 : C 0) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x)C (-pure x)) (Cm : ∀ (x y : FreeAddGroup α), C xC yC (x + y)) :
                                                                                  C z
                                                                                  theorem FreeGroup.induction_on {α : Type u} {C : FreeGroup αProp} (z : FreeGroup α) (C1 : C 1) (Cp : ∀ (x : α), C (pure x)) (Ci : ∀ (x : α), C (pure x)C (pure x)⁻¹) (Cm : ∀ (x y : FreeGroup α), C xC yC (x * y)) :
                                                                                  C z
                                                                                  theorem FreeAddGroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                                                                                  f <$> pure x = pure (f x)
                                                                                  theorem FreeGroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                                                                                  f <$> pure x = pure (f x)
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.map_zero {α : Type u} {β : Type u} (f : αβ) :
                                                                                  f <$> 0 = 0
                                                                                  @[simp]
                                                                                  theorem FreeGroup.map_one {α : Type u} {β : Type u} (f : αβ) :
                                                                                  f <$> 1 = 1
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.map_add {α : Type u} {β : Type u} (f : αβ) (x : FreeAddGroup α) (y : FreeAddGroup α) :
                                                                                  f <$> (x + y) = f <$> x + f <$> y
                                                                                  @[simp]
                                                                                  theorem FreeGroup.map_mul {α : Type u} {β : Type u} (f : αβ) (x : FreeGroup α) (y : FreeGroup α) :
                                                                                  f <$> (x * y) = f <$> x * f <$> y
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.map_neg {α : Type u} {β : Type u} (f : αβ) (x : FreeAddGroup α) :
                                                                                  f <$> (-x) = -f <$> x
                                                                                  @[simp]
                                                                                  theorem FreeGroup.map_inv {α : Type u} {β : Type u} (f : αβ) (x : FreeGroup α) :
                                                                                  f <$> x⁻¹ = (f <$> x)⁻¹
                                                                                  theorem FreeAddGroup.pure_bind {α : Type u} {β : Type u} (f : αFreeAddGroup β) (x : α) :
                                                                                  pure x >>= f = f x
                                                                                  theorem FreeGroup.pure_bind {α : Type u} {β : Type u} (f : αFreeGroup β) (x : α) :
                                                                                  pure x >>= f = f x
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.zero_bind {α : Type u} {β : Type u} (f : αFreeAddGroup β) :
                                                                                  0 >>= f = 0
                                                                                  @[simp]
                                                                                  theorem FreeGroup.one_bind {α : Type u} {β : Type u} (f : αFreeGroup β) :
                                                                                  1 >>= f = 1
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.add_bind {α : Type u} {β : Type u} (f : αFreeAddGroup β) (x : FreeAddGroup α) (y : FreeAddGroup α) :
                                                                                  x + y >>= f = (x >>= f) + (y >>= f)
                                                                                  @[simp]
                                                                                  theorem FreeGroup.mul_bind {α : Type u} {β : Type u} (f : αFreeGroup β) (x : FreeGroup α) (y : FreeGroup α) :
                                                                                  x * y >>= f = (x >>= f) * (y >>= f)
                                                                                  @[simp]
                                                                                  theorem FreeAddGroup.neg_bind {α : Type u} {β : Type u} (f : αFreeAddGroup β) (x : FreeAddGroup α) :
                                                                                  -x >>= f = -(x >>= f)
                                                                                  @[simp]
                                                                                  theorem FreeGroup.inv_bind {α : Type u} {β : Type u} (f : αFreeGroup β) (x : FreeGroup α) :
                                                                                  x⁻¹ >>= f = (x >>= f)⁻¹
                                                                                  def FreeAddGroup.reduce {α : Type u} [DecidableEq α] (L : List (α × Bool)) :
                                                                                  List (α × Bool)

                                                                                  The maximal reduction of a word. It is computable iff α has decidable equality.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    def FreeGroup.reduce {α : Type u} [DecidableEq α] (L : List (α × Bool)) :
                                                                                    List (α × Bool)

                                                                                    The maximal reduction of a word. It is computable iff α has decidable equality.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem FreeAddGroup.reduce.cons {α : Type u} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) :
                                                                                      FreeAddGroup.reduce (x :: L) = List.casesOn (FreeAddGroup.reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 x.2 = !hd.2 then tl else x :: hd :: tl
                                                                                      @[simp]
                                                                                      theorem FreeGroup.reduce.cons {α : Type u} {L : List (α × Bool)} [DecidableEq α] (x : α × Bool) :
                                                                                      FreeGroup.reduce (x :: L) = List.casesOn (FreeGroup.reduce L) [x] fun (hd : α × Bool) (tl : List (α × Bool)) => if x.1 = hd.1 x.2 = !hd.2 then tl else x :: hd :: tl

                                                                                      The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

                                                                                      The first theorem that characterises the function reduce: a word reduces to its maximal reduction.

                                                                                      theorem FreeAddGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {x : α} {b : Bool} :
                                                                                      FreeAddGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃p
                                                                                      abbrev FreeAddGroup.reduce.not.match_1 {α : Type u_1} (motive : List (α × Bool)List (α × Bool)List (α × Bool)αBoolProp) :
                                                                                      ∀ (x x_1 x_2 : List (α × Bool)) (x_3 : α) (x_4 : Bool), (∀ (L2 L3 : List (α × Bool)) (x : α) (x_5 : Bool), motive [] L2 L3 x x_5)(∀ (x : α) (b : Bool) (L1 L2 L3 : List (α × Bool)) (x' : α) (b' : Bool), motive ((x, b) :: L1) L2 L3 x' b')motive x x_1 x_2 x_3 x_4
                                                                                      Equations
                                                                                      • =
                                                                                      Instances For
                                                                                        theorem FreeGroup.reduce.not {α : Type u} [DecidableEq α] {p : Prop} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} {x : α} {b : Bool} :
                                                                                        FreeGroup.reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃p
                                                                                        theorem FreeAddGroup.reduce.min {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red (FreeAddGroup.reduce L₁) L₂) :

                                                                                        The second theorem that characterises the function reduce: the maximal reduction of a word only reduces to itself.

                                                                                        theorem FreeGroup.reduce.min {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red (FreeGroup.reduce L₁) L₂) :

                                                                                        The second theorem that characterises the function reduce: the maximal reduction of a word only reduces to itself.

                                                                                        @[simp]

                                                                                        reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

                                                                                        @[simp]

                                                                                        reduce is idempotent, i.e. the maximal reduction of the maximal reduction of a word is the maximal reduction of the word.

                                                                                        theorem FreeAddGroup.reduce.Step.eq {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red.Step L₁ L₂) :
                                                                                        abbrev FreeAddGroup.reduce.Step.eq.match_1 {α : Type u_1} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (motive : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂)Prop) :
                                                                                        ∀ (x : Relation.Join FreeAddGroup.Red (FreeAddGroup.reduce L₁) (FreeAddGroup.reduce L₂)), (∀ (_L₃ : List (α × Bool)) (HR13 : FreeAddGroup.Red (FreeAddGroup.reduce L₁) _L₃) (HR23 : FreeAddGroup.Red (FreeAddGroup.reduce L₂) _L₃), motive )motive x
                                                                                        Equations
                                                                                        • =
                                                                                        Instances For
                                                                                          theorem FreeGroup.reduce.Step.eq {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red.Step L₁ L₂) :
                                                                                          theorem FreeAddGroup.reduce.eq_of_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) :

                                                                                          If a word reduces to another word, then they have a common maximal reduction.

                                                                                          theorem FreeGroup.reduce.eq_of_red {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :

                                                                                          If a word reduces to another word, then they have a common maximal reduction.

                                                                                          theorem FreeGroup.red.reduce_eq {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :

                                                                                          Alias of FreeGroup.reduce.eq_of_red.


                                                                                          If a word reduces to another word, then they have a common maximal reduction.

                                                                                          theorem FreeGroup.freeAddGroup.red.reduce_eq {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) :

                                                                                          Alias of FreeAddGroup.reduce.eq_of_red.


                                                                                          If a word reduces to another word, then they have a common maximal reduction.

                                                                                          theorem FreeAddGroup.Red.reduce_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (h : FreeAddGroup.Red L₁ L₂) :
                                                                                          theorem FreeGroup.Red.reduce_right {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (h : FreeGroup.Red L₁ L₂) :
                                                                                          theorem FreeAddGroup.Red.reduce_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (h : FreeAddGroup.Red L₁ L₂) :
                                                                                          theorem FreeGroup.Red.reduce_left {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (h : FreeGroup.Red L₁ L₂) :
                                                                                          theorem FreeAddGroup.reduce.sound {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.mk L₁ = FreeAddGroup.mk L₂) :

                                                                                          If two words correspond to the same element in the additive free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.

                                                                                          abbrev FreeAddGroup.reduce.sound.match_1 {α : Type u_1} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} (motive : Relation.Join FreeAddGroup.Red L₁ L₂Prop) :
                                                                                          ∀ (x : Relation.Join FreeAddGroup.Red L₁ L₂), (∀ (_L₃ : List (α × Bool)) (H13 : FreeAddGroup.Red L₁ _L₃) (H23 : FreeAddGroup.Red L₂ _L₃), motive )motive x
                                                                                          Equations
                                                                                          • =
                                                                                          Instances For
                                                                                            theorem FreeGroup.reduce.sound {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.mk L₁ = FreeGroup.mk L₂) :

                                                                                            If two words correspond to the same element in the free group, then they have a common maximal reduction. This is the proof that the function that sends an element of the free group to its maximal reduction is well-defined.

                                                                                            theorem FreeAddGroup.reduce.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂) :

                                                                                            If two words have a common maximal reduction, then they correspond to the same element in the additive free group.

                                                                                            theorem FreeGroup.reduce.exact {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.reduce L₁ = FreeGroup.reduce L₂) :

                                                                                            If two words have a common maximal reduction, then they correspond to the same element in the free group.

                                                                                            A word and its maximal reduction correspond to the same element of the additive free group.

                                                                                            A word and its maximal reduction correspond to the same element of the free group.

                                                                                            theorem FreeAddGroup.reduce.rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeAddGroup.Red L₁ L₂) :

                                                                                            If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal reduction of w₁.

                                                                                            theorem FreeGroup.reduce.rev {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :

                                                                                            If words w₁ w₂ are such that w₁ reduces to w₂, then w₂ reduces to the maximal reduction of w₁.

                                                                                            The function that sends an element of the additive free group to its maximal reduction.

                                                                                            Equations
                                                                                            • FreeAddGroup.toWord = Quot.lift FreeAddGroup.reduce
                                                                                            Instances For
                                                                                              theorem FreeAddGroup.toWord.proof_1 {α : Type u_1} [DecidableEq α] (_L₁ : List (α × Bool)) (_L₂ : List (α × Bool)) (H : FreeAddGroup.Red.Step _L₁ _L₂) :
                                                                                              def FreeGroup.toWord {α : Type u} [DecidableEq α] :
                                                                                              FreeGroup αList (α × Bool)

                                                                                              The function that sends an element of the free group to its maximal reduction.

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem FreeAddGroup.toWord_injective {α : Type u} [DecidableEq α] :
                                                                                                Function.Injective FreeAddGroup.toWord
                                                                                                @[simp]
                                                                                                @[simp]
                                                                                                @[simp]
                                                                                                @[simp]
                                                                                                theorem FreeGroup.toWord_eq_nil_iff {α : Type u} [DecidableEq α] {x : FreeGroup α} :
                                                                                                theorem FreeAddGroup.reduce.churchRosser.proof_1 {α : Type u_1} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} [DecidableEq α] (H12 : FreeAddGroup.Red L₁ L₂) (H13 : FreeAddGroup.Red L₁ L₃) :
                                                                                                def FreeAddGroup.reduce.churchRosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} [DecidableEq α] (H12 : FreeAddGroup.Red L₁ L₂) (H13 : FreeAddGroup.Red L₁ L₃) :
                                                                                                { L₄ : List (α × Bool) // FreeAddGroup.Red L₂ L₄ FreeAddGroup.Red L₃ L₄ }

                                                                                                Constructive Church-Rosser theorem (compare church_rosser).

                                                                                                Equations
                                                                                                Instances For
                                                                                                  def FreeGroup.reduce.churchRosser {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} {L₃ : List (α × Bool)} [DecidableEq α] (H12 : FreeGroup.Red L₁ L₂) (H13 : FreeGroup.Red L₁ L₃) :
                                                                                                  { L₄ : List (α × Bool) // FreeGroup.Red L₂ L₄ FreeGroup.Red L₃ L₄ }

                                                                                                  Constructive Church-Rosser theorem (compare church_rosser).

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    Equations
                                                                                                    instance FreeGroup.Red.decidableRel {α : Type u} [DecidableEq α] :
                                                                                                    DecidableRel FreeGroup.Red
                                                                                                    Equations
                                                                                                    def FreeGroup.Red.enum {α : Type u} [DecidableEq α] (L₁ : List (α × Bool)) :
                                                                                                    List (List (α × Bool))

                                                                                                    A list containing every word that w₁ reduces to.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      theorem FreeGroup.Red.enum.sound {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : L₂ List.filter (fun (b : List (α × Bool)) => decide (FreeGroup.Red L₁ b)) (List.sublists L₁)) :
                                                                                                      FreeGroup.Red L₁ L₂
                                                                                                      theorem FreeGroup.Red.enum.complete {α : Type u} {L₁ : List (α × Bool)} {L₂ : List (α × Bool)} [DecidableEq α] (H : FreeGroup.Red L₁ L₂) :
                                                                                                      instance FreeGroup.instFintypeSubtypeListProdBoolRed {α : Type u} {L₁ : List (α × Bool)} [DecidableEq α] :
                                                                                                      Fintype { L₂ : List (α × Bool) // FreeGroup.Red L₁ L₂ }
                                                                                                      Equations
                                                                                                      def FreeAddGroup.norm {α : Type u} [DecidableEq α] (x : FreeAddGroup α) :

                                                                                                      The length of reduced words provides a norm on an additive free group.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def FreeGroup.norm {α : Type u} [DecidableEq α] (x : FreeGroup α) :

                                                                                                        The length of reduced words provides a norm on a free group.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          @[simp]
                                                                                                          theorem FreeGroup.norm_eq_zero {α : Type u} [DecidableEq α] {x : FreeGroup α} :
                                                                                                          @[simp]