Documentation

Mathlib.GroupTheory.Coset.Basic

Cosets #

This file develops the basic theory of left and right cosets.

When G is a group and a : G, s : Set G, with open scoped Pointwise we can write:

If instead G is an additive group, we can write (with open scoped Pointwise still)

Main definitions #

Notation #

TODO #

Properly merge with pointwise actions on sets, by renaming and deduplicating lemmas as appropriate.

theorem mem_leftAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a + x a +ᵥ s
theorem mem_leftCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a * x a s
theorem mem_rightAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
theorem mem_rightCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
def LeftAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

Equality of two left cosets a + s and b + s.

Equations
Instances For
    def LeftCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

    Equality of two left cosets a * s and b * s.

    Equations
    Instances For
      def RightAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) :

      Equality of two right cosets s + a and s + b.

      Equations
      Instances For
        def RightCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) :

        Equality of two right cosets s * a and s * b.

        Equations
        Instances For
          theorem leftAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
          a +ᵥ (b +ᵥ s) = a + b +ᵥ s
          theorem leftCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
          a b s = (a * b) s
          theorem rightAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
          theorem rightCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
          theorem leftAddCoset_rightAddCoset {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) :
          theorem leftCoset_rightCoset {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) :
          theorem zero_leftAddCoset {α : Type u_1} [AddMonoid α] (s : Set α) :
          0 +ᵥ s = s
          theorem one_leftCoset {α : Type u_1} [Monoid α] (s : Set α) :
          1 s = s
          theorem rightAddCoset_zero {α : Type u_1} [AddMonoid α] (s : Set α) :
          theorem rightCoset_one {α : Type u_1} [Monoid α] (s : Set α) :
          theorem mem_own_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) :
          a a +ᵥ s
          theorem mem_own_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) :
          a a s
          theorem mem_own_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) :
          theorem mem_own_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) :
          theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : a +ᵥ s = s) :
          a s
          theorem mem_leftCoset_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : a s = s) :
          a s
          theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : AddOpposite.op a +ᵥ s = s) :
          a s
          theorem mem_rightCoset_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : MulOpposite.op a s = s) :
          a s
          theorem mem_leftAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) :
          x a +ᵥ s -a + x s
          theorem mem_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) :
          x a s a⁻¹ * x s
          theorem mem_rightAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) :
          theorem mem_rightCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) :
          theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
          a +ᵥ s = s
          theorem leftCoset_mem_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
          a s = s
          theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
          AddOpposite.op a +ᵥ s = s
          theorem rightCoset_mem_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
          MulOpposite.op a s = s
          theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) :
          theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) (a : α) :
          theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a s) :
          AddAction.orbit (↥s) a = s
          theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a s) :
          MulAction.orbit (↥s) a = s
          theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
          AddAction.orbit (↥s) 0 = s
          theorem orbit_subgroup_one_eq_self {α : Type u_1} [Group α] (s : Subgroup α) :
          MulAction.orbit (↥s) 1 = s
          theorem eq_addCosets_of_normal {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (N : s.Normal) (g : α) :
          g +ᵥ s = AddOpposite.op g +ᵥ s
          theorem eq_cosets_of_normal {α : Type u_1} [Group α] (s : Subgroup α) (N : s.Normal) (g : α) :
          g s = MulOpposite.op g s
          theorem normal_of_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), g +ᵥ s = AddOpposite.op g +ᵥ s) :
          s.Normal
          theorem normal_of_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) (h : ∀ (g : α), g s = MulOpposite.op g s) :
          s.Normal
          theorem normal_iff_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
          s.Normal ∀ (g : α), g +ᵥ s = AddOpposite.op g +ᵥ s
          theorem normal_iff_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) :
          s.Normal ∀ (g : α), g s = MulOpposite.op g s
          theorem leftAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
          x +ᵥ s = y +ᵥ s -x + y s
          theorem leftCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} :
          x s = y s x⁻¹ * y s
          theorem rightAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} :
          theorem rightCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} :
          def QuotientAddGroup.leftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

          The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

          Equations
          Instances For
            def QuotientGroup.leftRel {α : Type u_1} [Group α] (s : Subgroup α) :

            The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

            Equations
            Instances For
              theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
              theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
              theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
              (QuotientAddGroup.leftRel s) = fun (x y : α) => -x + y s
              theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
              (QuotientGroup.leftRel s) = fun (x y : α) => x⁻¹ * y s
              theorem QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
              Decidable ((QuotientAddGroup.leftRel s) x y) = Decidable ((fun (x y : α) => -x + y s) x y)
              Equations
              instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
              Equations

              α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

              Equations

              α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

              Equations
              def QuotientAddGroup.rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :

              The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

              Equations
              Instances For
                def QuotientGroup.rightRel {α : Type u_1} [Group α] (s : Subgroup α) :

                The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

                Equations
                Instances For
                  theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} :
                  theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
                  theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
                  (QuotientAddGroup.rightRel s) = fun (x y : α) => y + -x s
                  theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
                  (QuotientGroup.rightRel s) = fun (x y : α) => y * x⁻¹ s
                  Equations
                  theorem QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
                  Decidable ((QuotientAddGroup.rightRel s) x y) = Decidable ((fun (x y : α) => y + -x s) x y)
                  instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
                  Equations
                  theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
                  (QuotientAddGroup.leftRel s) a b(QuotientAddGroup.rightRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)
                  theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α s) :
                  Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g
                  theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
                  (QuotientAddGroup.rightRel s) a b(QuotientAddGroup.leftRel s) ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)
                  theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : Quotient (QuotientAddGroup.rightRel s)) :
                  Quotient.map' (fun (g : α) => -g) (Quotient.map' (fun (g : α) => -g) g) = g

                  Right cosets are in bijection with left cosets.

                  Equations
                  Instances For

                    Right cosets are in bijection with left cosets.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev QuotientAddGroup.mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α) :
                      α s

                      The canonical map from an AddGroup α to the quotient α ⧸ s.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev QuotientGroup.mk {α : Type u_1} [Group α] {s : Subgroup α} (a : α) :
                        α s

                        The canonical map from a group α to the quotient α ⧸ s.

                        Equations
                        Instances For
                          theorem QuotientAddGroup.mk_surjective {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
                          Function.Surjective QuotientAddGroup.mk
                          theorem QuotientGroup.mk_surjective {α : Type u_1} [Group α] {s : Subgroup α} :
                          Function.Surjective QuotientGroup.mk
                          @[simp]
                          theorem QuotientAddGroup.range_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
                          Set.range QuotientAddGroup.mk = Set.univ
                          @[simp]
                          theorem QuotientGroup.range_mk {α : Type u_1} [Group α] {s : Subgroup α} :
                          Set.range QuotientGroup.mk = Set.univ
                          theorem QuotientAddGroup.induction_on {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                          C x
                          theorem QuotientGroup.induction_on {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                          C x
                          instance QuotientAddGroup.instCoeQuotientAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
                          Coe α (α s)
                          Equations
                          • QuotientAddGroup.instCoeQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
                          instance QuotientGroup.instCoeQuotientSubgroup {α : Type u_1} [Group α] {s : Subgroup α} :
                          Coe α (α s)
                          Equations
                          • QuotientGroup.instCoeQuotientSubgroup = { coe := QuotientGroup.mk }
                          @[deprecated]
                          theorem QuotientGroup.induction_on' {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                          C x

                          Alias of QuotientGroup.induction_on.

                          @[deprecated]
                          theorem QuotientAddGroup.induction_on' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} (x : α s) (H : ∀ (z : α), C z) :
                          C x
                          @[simp]
                          theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (QuotientAddGroup.leftRel s) a bf a = f b) (x : α) :
                          Quotient.liftOn' (↑x) f h = f x
                          @[simp]
                          theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [Group α] {s : Subgroup α} {β : Sort u_2} (f : αβ) (h : ∀ (a b : α), (QuotientGroup.leftRel s) a bf a = f b) (x : α) :
                          Quotient.liftOn' (↑x) f h = f x
                          theorem QuotientAddGroup.forall_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
                          (∀ (x : α s), C x) ∀ (x : α), C x
                          theorem QuotientGroup.forall_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
                          (∀ (x : α s), C x) ∀ (x : α), C x
                          theorem QuotientAddGroup.exists_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α sProp} :
                          (∃ (x : α s), C x) ∃ (x : α), C x
                          theorem QuotientGroup.exists_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α sProp} :
                          (∃ (x : α s), C x) ∃ (x : α), C x
                          theorem QuotientAddGroup.eq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
                          a = b -a + b s
                          theorem QuotientGroup.eq {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} :
                          a = b a⁻¹ * b s
                          @[deprecated]
                          theorem QuotientGroup.eq' {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} :
                          a = b a⁻¹ * b s

                          Alias of QuotientGroup.eq.

                          @[deprecated]
                          theorem QuotientAddGroup.eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} :
                          a = b -a + b s
                          theorem QuotientAddGroup.out_eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α s) :
                          (Quotient.out' a) = a
                          theorem QuotientGroup.out_eq' {α : Type u_1} [Group α] {s : Subgroup α} (a : α s) :
                          (Quotient.out' a) = a
                          theorem QuotientAddGroup.strictMono_comap_prod_image {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
                          StrictMono fun (t : AddSubgroup α) => (AddSubgroup.comap s.subtype t, QuotientAddGroup.mk '' t)

                          Given an additive subgroup s, the function that sends an additive subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

                          theorem QuotientGroup.strictMono_comap_prod_image {α : Type u_1} [Group α] (s : Subgroup α) :
                          StrictMono fun (t : Subgroup α) => (Subgroup.comap s.subtype t, QuotientGroup.mk '' t)

                          Given a subgroup s, the function that sends a subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

                          theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) :
                          ∃ (h : s), Quotient.out' g = g + h
                          theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [Group α] (s : Subgroup α) (g : α) :
                          ∃ (h : s), Quotient.out' g = g * h
                          @[simp]
                          theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b s) :
                          (a + b) = a
                          @[simp]
                          theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [Group α] {s : Subgroup α} {b : α} (a : α) (hb : b s) :
                          (a * b) = a
                          theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) :
                          {x : α | x = g} = g +ᵥ s
                          theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) (g : α) :
                          {x : α | x = g} = g s
                          theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                          QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) ⁻¹' s
                          theorem QuotientGroup.preimage_image_mk {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                          QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) ⁻¹' s
                          theorem QuotientAddGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                          QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 + x) '' s
                          theorem QuotientGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                          QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : N), (fun (x_1 : α) => x_1 * x) '' s
                          theorem QuotientAddGroup.preimage_image_mk_eq_add {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) :
                          QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = s + N
                          theorem QuotientGroup.preimage_image_mk_eq_mul {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) :
                          QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = s * N
                          theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                          ∀ (x : s), (fun (x : (g +ᵥ s)) => -g + x, ) ((fun (x : s) => g + x, ) x) = x
                          theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (g +ᵥ s)) :
                          -g + x s
                          def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                          (g +ᵥ s) s

                          The natural bijection between the cosets g + s and s.

                          Equations
                          Instances For
                            theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : s) :
                            as, (fun (x : α) => g +ᵥ x) a = g + x
                            theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                            ∀ (x : (g +ᵥ s)), (fun (x : s) => g + x, ) ((fun (x : (g +ᵥ s)) => -g + x, ) x) = x
                            def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) :
                            (g s) s

                            The natural bijection between a left coset g * s and s.

                            Equations
                            Instances For
                              def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                              (AddOpposite.op g +ᵥ s) s

                              The natural bijection between the cosets s + g and s.

                              Equations
                              Instances For
                                theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                                ∀ (x : s), (fun (x : (AddOpposite.op g +ᵥ s)) => x + -g, ) ((fun (x : s) => x + g, ) x) = x
                                theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (AddOpposite.op g +ᵥ s)) :
                                x + -g s
                                theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                                ∀ (x : (AddOpposite.op g +ᵥ s)), (fun (x : s) => x + g, ) ((fun (x : (AddOpposite.op g +ᵥ s)) => x + -g, ) x) = x
                                theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : s) :
                                as, (fun (x : α) => AddOpposite.op g +ᵥ x) a = x + g
                                def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) :
                                (MulOpposite.op g s) s

                                The natural bijection between a right coset s * g and s.

                                Equations
                                Instances For
                                  theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α s) :
                                  ({ x : α // x = L } (Quotient.out' L +ᵥ s)) = ({ x : α // x = L } {x : α | x = (Quotient.out' L)})
                                  theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α s) :
                                  ({ x : α // Quotient.mk'' x = L } { x : α // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }) = ({ x : α // Quotient.mk'' x = L } { x : α // Quotient.mk'' x = L })
                                  noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} :
                                  α (α s) × s

                                  A (non-canonical) bijection between an add_group α and the product (α/s) × s

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [Group α] {s : Subgroup α} :
                                    α (α s) × s

                                    A (non-canonical) bijection between a group α and the product (α/s) × s

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel s) _a _b) :
                                      def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) :
                                      α s α t

                                      If two subgroups M and N of G are equal, their quotients are in bijection.

                                      Equations
                                      Instances For
                                        theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : (QuotientAddGroup.leftRel t) _a _b) :
                                        theorem AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α t) :
                                        Quotient.map' id (Quotient.map' id q) = q
                                        theorem AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α s) :
                                        Quotient.map' id (Quotient.map' id q) = q
                                        def Subgroup.quotientEquivOfEq {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) :
                                        α s α t

                                        If two subgroups M and N of G are equal, their quotients are in bijection.

                                        Equations
                                        Instances For
                                          theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) (a : α) :
                                          theorem AddSubgroup.quotientEquivSumOfLE'.proof_5 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : Quotient (QuotientAddGroup.leftRel s)) :
                                          (fun (a : (α t) × t s.addSubgroupOf t) => Quotient.map' (fun (b : t) => f a.1 + b) a.2) ((fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)) q) = q
                                          theorem AddSubgroup.quotientEquivSumOfLE'.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (f : α tα) (a : (α t) × t s.addSubgroupOf t) (b : t) (c : t) (h : (QuotientAddGroup.leftRel (s.addSubgroupOf t)) b c) :
                                          (QuotientAddGroup.leftRel s) ((fun (b : t) => f a.1 + b) b) ((fun (b : t) => f a.1 + b) c)
                                          theorem AddSubgroup.quotientEquivSumOfLE'.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (b : α) (c : α) (h : (QuotientAddGroup.leftRel s) b c) :
                                          def AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) :
                                          α s (α t) × t s.addSubgroupOf t

                                          If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is AddSubgroup.quotientEquivSumOfLE.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem AddSubgroup.quotientEquivSumOfLE'.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (b : α) (c : α) (h : (QuotientAddGroup.leftRel s) b c) :
                                            (QuotientAddGroup.leftRel (s.addSubgroupOf t)) ((fun (g : α) => -f (Quotient.mk'' g) + g, ) b) ((fun (g : α) => -f (Quotient.mk'' g) + g, ) c)
                                            theorem AddSubgroup.quotientEquivSumOfLE'.proof_6 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t✝) (f : α t✝α) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α t✝) × t✝ s.addSubgroupOf t✝) :
                                            (fun (a : α s) => (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)) ((fun (a : (α t✝) × t✝ s.addSubgroupOf t✝) => Quotient.map' (fun (b : t✝) => f a.1 + b) a.2) t) = t
                                            theorem AddSubgroup.quotientEquivSumOfLE'.proof_2 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) :
                                            -f (Quotient.mk'' g) + g t
                                            @[simp]
                                            theorem Subgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α t) × t s.subgroupOf t) :
                                            (Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun (b : t) => f a.1 * b) a.2
                                            @[simp]
                                            theorem AddSubgroup.quotientEquivSumOfLE'_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α t) × t s.addSubgroupOf t) :
                                            (AddSubgroup.quotientEquivSumOfLE' h_le f hf).symm a = Quotient.map' (fun (b : t) => f a.1 + b) a.2
                                            @[simp]
                                            theorem Subgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : α s) :
                                            (Subgroup.quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => (f (Quotient.mk'' g))⁻¹ * g, ) a)
                                            @[simp]
                                            theorem AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α s) :
                                            (AddSubgroup.quotientEquivSumOfLE' h_le f hf) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -f (Quotient.mk'' g) + g, ) a)
                                            def Subgroup.quotientEquivProdOfLE' {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) :
                                            α s (α t) × t s.subgroupOf t

                                            If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is Subgroup.quotientEquivProdOfLE.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              noncomputable def AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) :
                                              α s (α t) × t s.addSubgroupOf t

                                              If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem AddSubgroup.quotientEquivSumOfLE_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : α s) :
                                                (AddSubgroup.quotientEquivSumOfLE h_le) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => -(Quotient.mk'' g).out' + g, ) a)
                                                @[simp]
                                                theorem Subgroup.quotientEquivProdOfLE_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : (α t) × t s.subgroupOf t) :
                                                (Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun (b : t) => Quotient.out' a.1 * b) a.2
                                                @[simp]
                                                theorem AddSubgroup.quotientEquivSumOfLE_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (a : (α t) × t s.addSubgroupOf t) :
                                                (AddSubgroup.quotientEquivSumOfLE h_le).symm a = Quotient.map' (fun (b : t) => Quotient.out' a.1 + b) a.2
                                                @[simp]
                                                theorem Subgroup.quotientEquivProdOfLE_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) (a : α s) :
                                                (Subgroup.quotientEquivProdOfLE h_le) a = (Quotient.map' id a, Quotient.map' (fun (g : α) => (Quotient.mk'' g).out'⁻¹ * g, ) a)
                                                noncomputable def Subgroup.quotientEquivProdOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s t) :
                                                α s (α t) × t s.subgroupOf t

                                                If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

                                                Equations
                                                Instances For
                                                  def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :
                                                  s H.addSubgroupOf s t H.addSubgroupOf t

                                                  If s ≤ t, then there is an embedding s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t.

                                                  Equations
                                                  Instances For
                                                    theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (q₁ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) (q₂ : Quotient (QuotientAddGroup.leftRel (H.addSubgroupOf s))) :
                                                    Quotient.map' (AddSubgroup.inclusion h) q₁ = Quotient.map' (AddSubgroup.inclusion h) q₂q₁ = q₂
                                                    theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : s) (b : s) :
                                                    (QuotientAddGroup.leftRel (H.addSubgroupOf s)) a b(QuotientAddGroup.leftRel (H.addSubgroupOf t)) ((AddSubgroup.inclusion h) a) ((AddSubgroup.inclusion h) b)
                                                    def Subgroup.quotientSubgroupOfEmbeddingOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
                                                    s H.subgroupOf s t H.subgroupOf t

                                                    If s ≤ t, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : s) :
                                                      def AddSubgroup.quotientAddSubgroupOfMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) :
                                                      H s.addSubgroupOf HH t.addSubgroupOf H

                                                      If s ≤ t, then there is a map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H.

                                                      Equations
                                                      Instances For
                                                        theorem AddSubgroup.quotientAddSubgroupOfMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (a : H) (b : H) :
                                                        (QuotientAddGroup.leftRel (s.addSubgroupOf H)) a b(QuotientAddGroup.leftRel (t.addSubgroupOf H)) (id a) (id b)
                                                        def Subgroup.quotientSubgroupOfMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) :
                                                        H s.subgroupOf HH t.subgroupOf H

                                                        If s ≤ t, then there is a map H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s t) (g : H) :
                                                          @[simp]
                                                          theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s t) (g : H) :
                                                          theorem AddSubgroup.quotientMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (a : α) (b : α) :
                                                          def AddSubgroup.quotientMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) :
                                                          α sα t

                                                          If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

                                                          Equations
                                                          Instances For
                                                            def Subgroup.quotientMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) :
                                                            α sα t

                                                            If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s t) (g : α) :
                                                              @[simp]
                                                              theorem Subgroup.quotientMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s t) (g : α) :
                                                              theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
                                                              iInf f f i
                                                              theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) (q₂ : Quotient (QuotientAddGroup.leftRel ((⨅ (i : ι), f i).addSubgroupOf H))) :
                                                              (fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H q) q₁ = (fun (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) => AddSubgroup.quotientAddSubgroupOfMapOfLE H q) q₂q₁ = q₂
                                                              def AddSubgroup.quotientiInfAddSubgroupOfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) :
                                                              H (⨅ (i : ι), f i).addSubgroupOf H (i : ι) → H (f i).addSubgroupOf H

                                                              The natural embedding H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (q : H (⨅ (i : ι), f i).addSubgroupOf H) (i : ι) :
                                                                @[simp]
                                                                theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) (q : H (⨅ (i : ι), f i).subgroupOf H) (i : ι) :
                                                                def Subgroup.quotientiInfSubgroupOfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) :
                                                                H (⨅ (i : ι), f i).subgroupOf H (i : ι) → H (f i).subgroupOf H

                                                                The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (H : AddSubgroup α) (g : H) (i : ι) :
                                                                  @[simp]
                                                                  theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (H : Subgroup α) (g : H) (i : ι) :
                                                                  theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
                                                                  iInf f f i
                                                                  theorem AddSubgroup.quotientiInfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) :
                                                                  (fun (q : α ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE q) q₁ = (fun (q : α ⨅ (i : ι), f i) (i : ι) => AddSubgroup.quotientMapOfLE q) q₂q₁ = q₂
                                                                  def AddSubgroup.quotientiInfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) :
                                                                  α ⨅ (i : ι), f i (i : ι) → α f i

                                                                  The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem AddSubgroup.quotientiInfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (q : α ⨅ (i : ι), f i) (i : ι) :
                                                                    @[simp]
                                                                    theorem Subgroup.quotientiInfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (q : α ⨅ (i : ι), f i) (i : ι) :
                                                                    def Subgroup.quotientiInfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) :
                                                                    α ⨅ (i : ι), f i (i : ι) → α f i

                                                                    The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (g : α) (i : ι) :
                                                                      @[simp]
                                                                      theorem Subgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ιSubgroup α) (g : α) (i : ι) :
                                                                      def AddMonoidHom.fiberEquivKer {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) :
                                                                      (f ⁻¹' {f a}) f.ker

                                                                      An equivalence between any non-empty fiber of an AddMonoidHom and its kernel.

                                                                      Equations
                                                                      Instances For
                                                                        theorem AddMonoidHom.fiberEquivKer.proof_1 {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) :
                                                                        f ⁻¹' {f a} = a +ᵥ f.ker
                                                                        def MonoidHom.fiberEquivKer {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) :
                                                                        (f ⁻¹' {f a}) f.ker

                                                                        An equivalence between any non-empty fiber of a MonoidHom and its kernel.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem AddMonoidHom.fiberEquivKer_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : (f ⁻¹' {f a})) :
                                                                          ((f.fiberEquivKer a) g) = -a + g
                                                                          @[simp]
                                                                          theorem MonoidHom.fiberEquivKer_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : (f ⁻¹' {f a})) :
                                                                          ((f.fiberEquivKer a) g) = a⁻¹ * g
                                                                          @[simp]
                                                                          theorem AddMonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (g : f.ker) :
                                                                          ((f.fiberEquivKer a).symm g) = a + g
                                                                          @[simp]
                                                                          theorem MonoidHom.fiberEquivKer_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (g : f.ker) :
                                                                          ((f.fiberEquivKer a).symm g) = a * g
                                                                          noncomputable def AddMonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) :
                                                                          (f ⁻¹' {h}) f.ker

                                                                          An equivalence between any fiber of a surjective AddMonoidHom and its kernel.

                                                                          Equations
                                                                          Instances For
                                                                            theorem AddMonoidHom.fiberEquivKerOfSurjective.proof_1 {α : Type u_2} [AddGroup α] {H : Type u_1} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) :
                                                                            f .choose = h
                                                                            noncomputable def MonoidHom.fiberEquivKerOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective f) (h : H) :
                                                                            (f ⁻¹' {h}) f.ker

                                                                            An equivalence between any fiber of a surjective MonoidHom and its kernel.

                                                                            Equations
                                                                            Instances For
                                                                              def AddMonoidHom.fiberEquiv {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) :
                                                                              (f ⁻¹' {f a}) (f ⁻¹' {f b})

                                                                              An equivalence between any two non-empty fibers of an AddMonoidHom.

                                                                              Equations
                                                                              • f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
                                                                              Instances For
                                                                                def MonoidHom.fiberEquiv {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) :
                                                                                (f ⁻¹' {f a}) (f ⁻¹' {f b})

                                                                                An equivalence between any two non-empty fibers of a MonoidHom.

                                                                                Equations
                                                                                • f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem AddMonoidHom.fiberEquiv_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) (g : (f ⁻¹' {f a})) :
                                                                                  ((f.fiberEquiv a b) g) = b + (-a + g)
                                                                                  @[simp]
                                                                                  theorem MonoidHom.fiberEquiv_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) (g : (f ⁻¹' {f a})) :
                                                                                  ((f.fiberEquiv a b) g) = b * (a⁻¹ * g)
                                                                                  @[simp]
                                                                                  theorem AddMonoidHom.fiberEquiv_symm_apply {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (a : α) (b : α) (g : (f ⁻¹' {f b})) :
                                                                                  ((f.fiberEquiv a b).symm g) = a + (-b + g)
                                                                                  @[simp]
                                                                                  theorem MonoidHom.fiberEquiv_symm_apply {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (a : α) (b : α) (g : (f ⁻¹' {f b})) :
                                                                                  ((f.fiberEquiv a b).symm g) = a * (b⁻¹ * g)
                                                                                  noncomputable def AddMonoidHom.fiberEquivOfSurjective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] {f : α →+ H} (hf : Function.Surjective f) (h : H) (h' : H) :
                                                                                  (f ⁻¹' {h}) (f ⁻¹' {h'})

                                                                                  An equivalence between any two fibers of a surjective AddMonoidHom.

                                                                                  Equations
                                                                                  Instances For
                                                                                    noncomputable def MonoidHom.fiberEquivOfSurjective {α : Type u_1} [Group α] {H : Type u_2} [Group H] {f : α →* H} (hf : Function.Surjective f) (h : H) (h' : H) :
                                                                                    (f ⁻¹' {h}) (f ⁻¹' {h'})

                                                                                    An equivalence between any two fibers of a surjective MonoidHom.

                                                                                    Equations
                                                                                    Instances For
                                                                                      noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
                                                                                      (QuotientAddGroup.mk ⁻¹' t) s × t

                                                                                      If s is a subgroup of the additive group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : s × t) :
                                                                                        (Quotient.out' a.2 + a.1) t
                                                                                        theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
                                                                                        a QuotientAddGroup.mk ⁻¹' t
                                                                                        theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
                                                                                        -Quotient.out' a + a s
                                                                                        theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
                                                                                        ∀ (x : s × t), (fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (-Quotient.out' a + a, , a, )) ((fun (a : s × t) => Quotient.out' a.2 + a.1, ) x) = x
                                                                                        theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) :
                                                                                        ∀ (x : (QuotientAddGroup.mk ⁻¹' t)), (fun (a : s × t) => Quotient.out' a.2 + a.1, ) ((fun (a : (QuotientAddGroup.mk ⁻¹' t)) => (-Quotient.out' a + a, , a, )) x) = x
                                                                                        noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [Group α] (s : Subgroup α) (t : Set (α s)) :
                                                                                        (QuotientGroup.mk ⁻¹' t) s × t

                                                                                        If s is a subgroup of the group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.

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