Documentation

Mathlib.GroupTheory.Coset

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
          @[inline]
          abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x a +ᵥ sProp) :
          ∀ (x_1 : x a +ᵥ s), (∀ (b : α) (hb : b s) (Eq : (fun (x : α) => a +ᵥ x) b = x), motive )motive x_1
          Equations
          • =
          Instances For
            theorem mem_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) :
            x a s a⁻¹ * x s
            @[inline]
            abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x AddOpposite.op a +ᵥ sProp) :
            ∀ (x_1 : x AddOpposite.op a +ᵥ s), (∀ (b : α) (hb : b s) (Eq : (fun (x : α) => AddOpposite.op a +ᵥ x) b = x), motive )motive x_1
            Equations
            • =
            Instances For
              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
              @[inline]
              abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b AddOpposite.op a +ᵥ sProp) :
              ∀ (x : _b AddOpposite.op a +ᵥ s), (∀ (c : α) (d : c s) (e : (fun (x : α) => AddOpposite.op a +ᵥ x) c = _b), motive )motive x
              Equations
              • =
              Instances For
                theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) :
                @[inline]
                abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b AddAction.orbit (↥s) aProp) :
                ∀ (x : _b AddAction.orbit (↥s) a), (∀ (c : s) (d : (fun (m : s) => m +ᵥ a) c = _b), motive )motive x
                Equations
                • =
                Instances For
                  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 : α} :
                      Setoid.r x y -x + y s
                      theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
                      theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
                      Setoid.r = fun (x y : α) => -x + y s
                      theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
                      Setoid.r = fun (x y : α) => x⁻¹ * y s
                      theorem QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
                      Decidable (Setoid.r x y) = Decidable ((fun (x y : α) => -x + y s) x y)
                      instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x s] :
                      DecidableRel Setoid.r
                      Equations
                      instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
                      DecidableRel Setoid.r
                      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 : α} :
                          Setoid.r x y y + -x s
                          theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} :
                          theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) :
                          Setoid.r = fun (x y : α) => y + -x s
                          theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) :
                          Setoid.r = fun (x y : α) => y * x⁻¹ s
                          theorem QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) :
                          Decidable (Setoid.r x y) = Decidable ((fun (x y : α) => y + -x s) x y)
                          instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x s] :
                          DecidableRel Setoid.r
                          Equations
                          instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun (x : α) => x s] :
                          DecidableRel Setoid.r
                          Equations
                          theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
                          Setoid.r a bSetoid.r ((fun (g : α) => -g) a) ((fun (g : α) => -g) b)

                          Right cosets are in bijection with left cosets.

                          Equations
                          Instances For
                            theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) :
                            Setoid.r a bSetoid.r ((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
                            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

                            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 : α), Setoid.r 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 : α), Setoid.r 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.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
                                  @[inline]
                                  abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x_1N, x + x_1 s)Prop) :
                                  ∀ (x_1 : x_1N, x + x_1 s), (∀ (z : α) (hz : z N) (hxz : x + z s), motive )motive x_1
                                  Equations
                                  • =
                                  Instances For
                                    @[inline]
                                    abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x_1s, -x_1 + x N)Prop) :
                                    ∀ (x_1 : x_1s, -x_1 + x N), (∀ (y : α) (hs : y s) (hN : -y + x N), motive )motive x_1
                                    Equations
                                    • =
                                    Instances For
                                      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
                                      @[inline]
                                      abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : (g +ᵥ s)Prop) :
                                      ∀ (x : (g +ᵥ s)), (∀ (x : α) (hx : x g +ᵥ s), motive x, hx)motive x
                                      Equations
                                      • =
                                      Instances For
                                        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_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) :
                                        ∀ (x : (g +ᵥ s)), (fun (x : s) => g + x, ) ((fun (x : (g +ᵥ s)) => -g + x, ) x) = x
                                        @[inline]
                                        abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (motive : sProp) :
                                        ∀ (x : s), (∀ (g : α) (hg : g s), motive g, hg)motive x
                                        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
                                          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_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (g +ᵥ s)) :
                                            -g + x s
                                            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
                                              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_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_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : s) :
                                              as, (fun (x : α) => AddOpposite.op g +ᵥ x) a = x + g
                                              @[inline]
                                              abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : (AddOpposite.op g +ᵥ s)Prop) :
                                              ∀ (x : (AddOpposite.op g +ᵥ s)), (∀ (x : α) (hx : x AddOpposite.op g +ᵥ s), motive x, hx)motive x
                                              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_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : (AddOpposite.op g +ᵥ s)) :
                                                  x + -g s
                                                  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)})
                                                    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
                                                      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 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_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α s) :
                                                        Quotient.map' id (Quotient.map' id q) = q
                                                        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_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_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
                                                          Setoid.r (id _a) (id _b)
                                                          theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
                                                          Setoid.r (id _a) (id _b)
                                                          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_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_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s t) (b : α) (c : α) (h : Setoid.r b c) :
                                                            Setoid.r (id b) (id c)
                                                            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 : Setoid.r b c) :
                                                            Setoid.r ((fun (b : t) => f a.1 + b) b) ((fun (b : t) => f a.1 + b) c)
                                                            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
                                                            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 : Setoid.r b c) :
                                                              Setoid.r ((fun (g : α) => -f (Quotient.mk'' g) + g, ) b) ((fun (g : α) => -f (Quotient.mk'' g) + g, ) c)
                                                              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 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)
                                                              @[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'_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'_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
                                                              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 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)
                                                                  @[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 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_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
                                                                  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
                                                                    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) :
                                                                    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
                                                                      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) :
                                                                          Setoid.r a bSetoid.r (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 : α) :
                                                                            Setoid.r a bSetoid.r (id a) (id 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
                                                                                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
                                                                                  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₂
                                                                                  @[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 : ι) :
                                                                                    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
                                                                                      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₂
                                                                                      theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ιAddSubgroup α) (i : ι) :
                                                                                      iInf f f i
                                                                                      @[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 : ι) :

                                                                                        Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.

                                                                                        theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :

                                                                                        Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.

                                                                                        theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :
                                                                                        theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (hf : Function.Injective f) :
                                                                                        theorem Subgroup.card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (hf : Function.Injective f) :
                                                                                        theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} (hHK : H K) :
                                                                                        theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} (hHK : H K) :
                                                                                        theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (K : AddSubgroup H) (f : α →+ H) (hf : Function.Injective f) :
                                                                                        theorem Subgroup.card_comap_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (K : Subgroup H) (f : α →* H) (hf : Function.Injective f) :
                                                                                        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
                                                                                                        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
                                                                                                        @[inline]
                                                                                                        abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (motive : (QuotientAddGroup.mk ⁻¹' t)Prop) :
                                                                                                        ∀ (x : (QuotientAddGroup.mk ⁻¹' t)), (∀ (a : α) (ha : a QuotientAddGroup.mk ⁻¹' t), motive a, ha)motive x
                                                                                                        Equations
                                                                                                        • =
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (motive : s × tProp) :
                                                                                                          ∀ (x : s × t), (∀ (a : α) (ha : a s) (x : α s) (hx : x t), motive (a, ha, x, hx))motive x
                                                                                                          Equations
                                                                                                          • =
                                                                                                          Instances For
                                                                                                            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_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : (QuotientAddGroup.mk ⁻¹' t)) :
                                                                                                            a QuotientAddGroup.mk ⁻¹' t
                                                                                                            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_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α s)) (a : s × t) :
                                                                                                            (Quotient.out' a.2 + a.1) t
                                                                                                            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
                                                                                                              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