Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes HΓΆlzl, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro,
Michael Howes

! This file was ported from Lean 3 source module deprecated.subgroup
! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Deprecated.Submonoid

/-!
# Unbundled subgroups (deprecated)

This file is deprecated, and is no longer imported by anything in mathlib other than other
deprecated files, and test files. You should not need to import it.

This file defines unbundled multiplicative and additive subgroups. Instead of using this file,

## Main definitions

`IsAddSubgroup (S : Set A)` : the predicate that `S` is the underlying subset of an additive
subgroup of `A`. The bundled variant `AddSubgroup A` should be used in preference to this.

`IsSubgroup (S : Set G)` : the predicate that `S` is the underlying subset of a subgroup
of `G`. The bundled variant `Subgroup G` should be used in preference to this.

## Tags

subgroup, subgroups, IsSubgroup
-/

open Set Function

variable {G: Type ?u.77632G : Type _: Type (?u.39733+1)Type _} {H: Type ?u.5H : Type _: Type (?u.5+1)Type _} {A: Type ?u.77638A : Type _: Type (?u.8+1)Type _} {a: Ga aβ: Gaβ aβ: Gaβ b: Gb c: Gc : G: Type ?u.77632G}

section Group

variable [Group: Type ?u.65 β Type ?u.65Group G: Type ?u.21G] [AddGroup: Type ?u.68 β Type ?u.68AddGroup A: Type ?u.2675A]

/-- `s` is an additive subgroup: a set containing 0 and closed under addition and negation. -/
structure IsAddSubgroup: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubmonoid s β (β {a : A}, a β s β -a β s) β IsAddSubgroup sIsAddSubgroup (s: Set As : Set: Type ?u.71 β Type ?u.71Set A: Type ?u.52A) extends IsAddSubmonoid: {A : Type ?u.75} β [inst : AddMonoid A] β Set A β PropIsAddSubmonoid s: Set As : Prop: TypeProp where
/-- The proposition that `s` is closed under negation. -/
neg_mem: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s β β {a : A}, a β s β -a β sneg_mem {a: ?m.371a} : a: ?m.371a β s: Set As β -a: ?m.371a β s: Set As

/-- `s` is a subgroup: a set containing 1 and closed under multiplication and inverse. -/
structure IsSubgroup: {G : Type u_1} β [inst : Group G] β Set G β PropIsSubgroup (s: Set Gs : Set: Type ?u.660 β Type ?u.660Set G: Type ?u.635G) extends IsSubmonoid: {M : Type ?u.664} β [inst : Monoid M] β Set M β PropIsSubmonoid s: Set Gs : Prop: TypeProp where
/-- The proposition that `s` is closed under inverse. -/
inv_mem: β {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem {a: ?m.990a} : a: ?m.990a β s: Set Gs β a: ?m.990aβ»ΒΉ β s: Set Gs
#align is_subgroup IsSubgroup: {G : Type u_1} β [inst : Group G] β Set G β PropIsSubgroup

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β β {x y : G}, x β s β y β s β x - y β sto_additive]
theorem IsSubgroup.div_mem: β {s : Set G}, IsSubgroup s β β {x y : G}, x β s β y β s β x / y β sIsSubgroup.div_mem {s: Set Gs : Set: Type ?u.1266 β Type ?u.1266Set G: Type ?u.1241G} (hs: IsSubgroup shs : IsSubgroup: {G : Type ?u.1269} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs) {x: Gx y: Gy : G: Type ?u.1241G} (hx: x β shx : x: Gx β s: Set Gs) (hy: y β shy : y: Gy β s: Set Gs) :
x: Gx / y: Gy β s: Set Gs := byGoals accomplished! π G: Type u_1H: Type ?u.1244A: Type ?u.1247a, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Ghs: IsSubgroup sx, y: Ghx: x β shy: y β sx / y β ssimpa only [div_eq_mul_inv: β {G : Type ?u.1606} [inst : DivInvMonoid G] (a b : G), a / b = a * bβ»ΒΉdiv_eq_mul_inv] using hs: IsSubgroup shs.mul_mem: β {M : Type ?u.1817} [inst : Monoid M] {s : Set M}, IsSubmonoid s β β {a b : M}, a β s β b β s β a * b β smul_mem hx: x β shx (hs: IsSubgroup shs.inv_mem: β {G : Type ?u.1833} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem hy: y β shy)Goals accomplished! π
#align is_subgroup.div_mem IsSubgroup.div_mem: β {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s β β {x y : G}, x β s β y β s β x / y β sIsSubgroup.div_mem
#align is_add_subgroup.sub_mem IsAddSubgroup.sub_mem: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β β {x y : G}, x β s β y β s β x - y β sIsAddSubgroup.sub_mem

theorem Additive.isAddSubgroup: β {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s β IsAddSubgroup sAdditive.isAddSubgroup {s: Set Gs : Set: Type ?u.2212 β Type ?u.2212Set G: Type ?u.2187G} (hs: IsSubgroup shs : IsSubgroup: {G : Type ?u.2215} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs) : @IsAddSubgroup: {A : Type ?u.2246} β [inst : AddGroup A] β Set A β PropIsAddSubgroup (Additive: Type ?u.2247 β Type ?u.2247Additive G: Type ?u.2187G) _ s: Set Gs :=

theorem Additive.isAddSubgroup_iff: β {s : Set G}, IsAddSubgroup s β IsSubgroup sAdditive.isAddSubgroup_iff {s: Set Gs : Set: Type ?u.2694 β Type ?u.2694Set G: Type ?u.2669G} : @IsAddSubgroup: {A : Type ?u.2697} β [inst : AddGroup A] β Set A β PropIsAddSubgroup (Additive: Type ?u.2698 β Type ?u.2698Additive G: Type ?u.2669G) _ s: Set Gs β IsSubgroup: {G : Type ?u.2715} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs :=

theorem Multiplicative.isSubgroup: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s β IsSubgroup sMultiplicative.isSubgroup {s: Set As : Set: Type ?u.3254 β Type ?u.3254Set A: Type ?u.3235A} (hs: IsAddSubgroup shs : IsAddSubgroup: {A : Type ?u.3257} β [inst : AddGroup A] β Set A β PropIsAddSubgroup s: Set As) :
@IsSubgroup: {G : Type ?u.3287} β [inst : Group G] β Set G β PropIsSubgroup (Multiplicative: Type ?u.3288 β Type ?u.3288Multiplicative A: Type ?u.3235A) _ s: Set As :=
#align multiplicative.is_subgroup Multiplicative.isSubgroup: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s β IsSubgroup sMultiplicative.isSubgroup

theorem Multiplicative.isSubgroup_iff: β {s : Set A}, IsSubgroup s β IsAddSubgroup sMultiplicative.isSubgroup_iff {s: Set As : Set: Type ?u.3706 β Type ?u.3706Set A: Type ?u.3687A} :
@IsSubgroup: {G : Type ?u.3709} β [inst : Group G] β Set G β PropIsSubgroup (Multiplicative: Type ?u.3710 β Type ?u.3710Multiplicative A: Type ?u.3687A) _ s: Set As β IsAddSubgroup: {A : Type ?u.3727} β [inst : AddGroup A] β Set A β PropIsAddSubgroup s: Set As :=
Multiplicative.isSubgroup: β {A : Type ?u.3749} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s β IsSubgroup sMultiplicative.isSubgroup h: ?m.3747hβ©
#align multiplicative.is_subgroup_iff Multiplicative.isSubgroup_iff: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsSubgroup s β IsAddSubgroup sMultiplicative.isSubgroup_iff

@[to_additive of_add_neg: β {G : Type u_1} [inst : AddGroup G] (s : Set G), 0 β s β (β {a b : G}, a β s β b β s β a + -b β s) β IsAddSubgroup sof_add_neg]
theorem IsSubgroup.of_div: β {G : Type u_1} [inst : Group G] (s : Set G), 1 β s β (β {a b : G}, a β s β b β s β a * bβ»ΒΉ β s) β IsSubgroup sIsSubgroup.of_div (s: Set Gs : Set: Type ?u.4236 β Type ?u.4236Set G: Type ?u.4211G) (one_mem: 1 β sone_mem : (1: ?m.42601 : G: Type ?u.4211G) β s: Set Gs)
(div_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sdiv_mem : β {a: Ga b: Gb : G: Type ?u.4211G}, a: Ga β s: Set Gs β b: Gb β s: Set Gs β a: Ga * b: Gbβ»ΒΉ β s: Set Gs) : IsSubgroup: {G : Type ?u.5484} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs :=
have inv_mem: β (a : G), a β s β aβ»ΒΉ β sinv_mem : β a: ?m.5520a, a: ?m.5520a β s: Set Gs β a: ?m.5520aβ»ΒΉ β s: Set Gs := fun a: ?m.5750a ha: ?m.5753ha => byGoals accomplished! π
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β saβ»ΒΉ β shave : 1: ?m.61201 * a: Gaβ»ΒΉ β s: Set Gs := div_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sdiv_mem one_mem: 1 β sone_mem ha: a β shaG: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β sthis: 1 * aβ»ΒΉ β saβ»ΒΉ β s
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β saβ»ΒΉ β sconvert this: 1 * aβ»ΒΉ β sthis using 1G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β sthis: 1 * aβ»ΒΉ β sh.e'_4aβ»ΒΉ = 1 * aβ»ΒΉ
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β saβ»ΒΉ β srw [G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β sthis: 1 * aβ»ΒΉ β sh.e'_4aβ»ΒΉ = 1 * aβ»ΒΉone_mul: β {M : Type ?u.7427} [inst : MulOneClass M] (a : M), 1 * a = aone_mulG: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sa: Gha: a β sthis: 1 * aβ»ΒΉ β sh.e'_4aβ»ΒΉ = aβ»ΒΉ]Goals accomplished! π
{ inv_mem := inv_mem: β (a : G), a β s β aβ»ΒΉ β sinv_mem _: G_
mul_mem := fun {a: ?m.6056a b: ?m.6059b} ha: ?m.6062ha hb: ?m.6065hb => byGoals accomplished! π
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sa * b β shave : a: Ga * b: Gbβ»ΒΉβ»ΒΉ β s: Set Gs := div_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sdiv_mem ha: a β sha (inv_mem: β (a : G), a β s β aβ»ΒΉ β sinv_mem b: Gb hb: b β shb)G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sthis: a * bβ»ΒΉβ»ΒΉ β sa * b β s
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sa * b β sconvert this: a * bβ»ΒΉβ»ΒΉ β sthisG: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sthis: a * bβ»ΒΉβ»ΒΉ β sh.e'_4.h.e'_6b = bβ»ΒΉβ»ΒΉ
G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sa * b β srw [G: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sthis: a * bβ»ΒΉβ»ΒΉ β sh.e'_4.h.e'_6b = bβ»ΒΉβ»ΒΉinv_inv: β {G : Type ?u.8927} [inst : InvolutiveInv G] (a : G), aβ»ΒΉβ»ΒΉ = ainv_invG: Type u_1H: Type ?u.4214A: Type ?u.4217aβ, aβ, aβ, bβ, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Gone_mem: 1 β sdiv_mem: β {a b : G}, a β s β b β s β a * bβ»ΒΉ β sinv_mem: β (a : G), a β s β aβ»ΒΉ β sa, b: Gha: a β shb: b β sthis: a * bβ»ΒΉβ»ΒΉ β sh.e'_4.h.e'_6b = b]Goals accomplished! π
one_mem: 1 β sone_mem }
#align is_subgroup.of_div IsSubgroup.of_div: β {G : Type u_1} [inst : Group G] (s : Set G), 1 β s β (β {a b : G}, a β s β b β s β a * bβ»ΒΉ β s) β IsSubgroup sIsSubgroup.of_div

theorem IsAddSubgroup.of_sub: β {A : Type u_1} [inst : AddGroup A] (s : Set A), 0 β s β (β {a b : A}, a β s β b β s β a - b β s) β IsAddSubgroup sIsAddSubgroup.of_sub (s: Set As : Set: Type ?u.9272 β Type ?u.9272Set A: Type ?u.9253A) (zero_mem: 0 β szero_mem : (0: ?m.92960 : A: Type ?u.9253A) β s: Set As)
(sub_mem: β {a b : A}, a β s β b β s β a - b β ssub_mem : β {a: Aa b: Ab : A: Type ?u.9253A}, a: Aa β s: Set As β b: Ab β s: Set As β a: Aa - b: Ab β s: Set As) : IsAddSubgroup: {A : Type ?u.10053} β [inst : AddGroup A] β Set A β PropIsAddSubgroup s: Set As :=
0 β s β (β {a b : G}, a β s β b β s β a + -b β s) β IsAddSubgroup sIsAddSubgroup.of_add_neg s: Set As zero_mem: 0 β szero_mem fun {x: ?m.10102x y: ?m.10105y} hx: ?m.10108hx hy: ?m.10111hy => byGoals accomplished! π
G: Type ?u.9247H: Type ?u.9250A: Type u_1a, aβ, aβ, b, c: GinstβΒΉ: Group Ginstβ: AddGroup As: Set Azero_mem: 0 β ssub_mem: β {a b : A}, a β s β b β s β a - b β sx, y: Ahx: x β shy: y β sx + -y β ssimpa only [sub_eq_add_neg: β {G : Type ?u.10135} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg] using sub_mem: β {a b : A}, a β s β b β s β a - b β ssub_mem hx: x β shx hy: y β shyGoals accomplished! π
#align is_add_subgroup.of_sub IsAddSubgroup.of_sub: β {A : Type u_1} [inst : AddGroup A] (s : Set A), 0 β s β (β {a b : A}, a β s β b β s β a - b β s) β IsAddSubgroup sIsAddSubgroup.of_sub

theorem IsSubgroup.inter: β {G : Type u_1} [inst : Group G] {sβ sβ : Set G}, IsSubgroup sβ β IsSubgroup sβ β IsSubgroup (sβ β© sβ)IsSubgroup.inter {sβ: Set Gsβ sβ: Set Gsβ : Set: Type ?u.10386 β Type ?u.10386Set G: Type ?u.10358G} (hsβ: IsSubgroup sβhsβ : IsSubgroup: {G : Type ?u.10389} β [inst : Group G] β Set G β PropIsSubgroup sβ: Set Gsβ) (hsβ: IsSubgroup sβhsβ : IsSubgroup: {G : Type ?u.10420} β [inst : Group G] β Set G β PropIsSubgroup sβ: Set Gsβ) :
IsSubgroup: {G : Type ?u.10446} β [inst : Group G] β Set G β PropIsSubgroup (sβ: Set Gsβ β© sβ: Set Gsβ) :=
{ IsSubmonoid.inter: β {M : Type ?u.10495} [inst : Monoid M] {sβ sβ : Set M}, IsSubmonoid sβ β IsSubmonoid sβ β IsSubmonoid (sβ β© sβ)IsSubmonoid.inter hsβ: IsSubgroup sβhsβ.toIsSubmonoid: β {G : Type ?u.10527} [inst : Group G] {s : Set G}, IsSubgroup s β IsSubmonoid stoIsSubmonoid hsβ: IsSubgroup sβhsβ.toIsSubmonoid: β {G : Type ?u.10549} [inst : Group G] {s : Set G}, IsSubgroup s β IsSubmonoid stoIsSubmonoid with
inv_mem := fun hx: ?m.10875hx => β¨hsβ: IsSubgroup sβhsβ.inv_mem: β {G : Type ?u.10885} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem hx: ?m.10875hx.1: β {a b : Prop}, a β§ b β a1, hsβ: IsSubgroup sβhsβ.inv_mem: β {G : Type ?u.10895} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem hx: ?m.10875hx.2: β {a b : Prop}, a β§ b β b2β© }
#align is_subgroup.inter IsSubgroup.inter: β {G : Type u_1} [inst : Group G] {sβ sβ : Set G}, IsSubgroup sβ β IsSubgroup sβ β IsSubgroup (sβ β© sβ)IsSubgroup.inter

@[to_additive: β {G : Type u_2} [inst : AddGroup G] {ΞΉ : Sort u_1} {s : ΞΉ β Set G},
theorem IsSubgroup.iInter: β {G : Type u_2} [inst : Group G] {ΞΉ : Sort u_1} {s : ΞΉ β Set G},
(β (y : ΞΉ), IsSubgroup (s y)) β IsSubgroup (Set.iInter s)IsSubgroup.iInter {ΞΉ: Sort u_1ΞΉ : Sort _: Type ?u.10978SortSort _: Type ?u.10978 _} {s: ΞΉ β Set Gs : ΞΉ: Sort ?u.10978ΞΉ β Set: Type ?u.10983 β Type ?u.10983Set G: Type ?u.10953G} (hs: β (y : ΞΉ), IsSubgroup (s y)hs : β y: ΞΉy : ΞΉ: Sort ?u.10978ΞΉ, IsSubgroup: {G : Type ?u.10990} β [inst : Group G] β Set G β PropIsSubgroup (s: ΞΉ β Set Gs y: ΞΉy)) :
IsSubgroup: {G : Type ?u.11022} β [inst : Group G] β Set G β PropIsSubgroup (Set.iInter: {Ξ² : Type ?u.11045} β {ΞΉ : Sort ?u.11044} β (ΞΉ β Set Ξ²) β Set Ξ²Set.iInter s: ΞΉ β Set Gs) :=
{ IsSubmonoid.iInter: β {M : Type ?u.11064} [inst : Monoid M] {ΞΉ : Sort ?u.11063} {s : ΞΉ β Set M},
(β (y : ΞΉ), IsSubmonoid (s y)) β IsSubmonoid (Set.iInter s)IsSubmonoid.iInter fun y: ?m.11097y => (hs: β (y : ΞΉ), IsSubgroup (s y)hs y: ?m.11097y).toIsSubmonoid: β {G : Type ?u.11099} [inst : Group G] {s : Set G}, IsSubgroup s β IsSubmonoid stoIsSubmonoid with
inv_mem := fun h: ?m.11461h =>
Set.mem_iInter: β {Ξ± : Type ?u.11463} {ΞΉ : Sort ?u.11464} {x : Ξ±} {s : ΞΉ β Set Ξ±}, (x β Set.iInter fun i => s i) β β (i : ΞΉ), x β s iSet.mem_iInter.2: β {a b : Prop}, (a β b) β b β a2 fun y: ?m.11481y => IsSubgroup.inv_mem: β {G : Type ?u.11483} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sIsSubgroup.inv_mem (hs: β (y : ΞΉ), IsSubgroup (s y)hs _: ΞΉ_) (Set.mem_iInter: β {Ξ± : Type ?u.11497} {ΞΉ : Sort ?u.11498} {x : Ξ±} {s : ΞΉ β Set Ξ±}, (x β Set.iInter fun i => s i) β β (i : ΞΉ), x β s iSet.mem_iInter.1: β {a b : Prop}, (a β b) β a β b1 h: ?m.11461h y: ?m.11481y) }
#align is_subgroup.Inter IsSubgroup.iInter: β {G : Type u_2} [inst : Group G] {ΞΉ : Sort u_1} {s : ΞΉ β Set G}, (β (y : ΞΉ), IsSubgroup (s y)) β IsSubgroup (iInter s)IsSubgroup.iInter
#align is_add_subgroup.Inter IsAddSubgroup.iInter: β {G : Type u_2} [inst : AddGroup G] {ΞΉ : Sort u_1} {s : ΞΉ β Set G},

@[to_additive: β {G : Type u_2} [inst : AddGroup G] {ΞΉ : Type u_1} [inst_1 : Nonempty ΞΉ] {s : ΞΉ β Set G},
(β (i : ΞΉ), IsAddSubgroup (s i)) β (β (i j : ΞΉ), β k, s i β s k β§ s j β s k) β IsAddSubgroup (iUnion fun i => s i)to_additive]
theorem isSubgroup_iUnion_of_directed: β {G : Type u_2} [inst : Group G] {ΞΉ : Type u_1} [inst_1 : Nonempty ΞΉ] {s : ΞΉ β Set G},
(β (i : ΞΉ), IsSubgroup (s i)) β (β (i j : ΞΉ), β k, s i β s k β§ s j β s k) β IsSubgroup (iUnion fun i => s i)isSubgroup_iUnion_of_directed {ΞΉ: Type u_1ΞΉ : Type _: Type (?u.11620+1)Type _} [Nonempty: Sort ?u.11623 β PropNonempty ΞΉ: Type ?u.11620ΞΉ] {s: ΞΉ β Set Gs : ΞΉ: Type ?u.11620ΞΉ β Set: Type ?u.11628 β Type ?u.11628Set G: Type ?u.11595G}
(hs: β (i : ΞΉ), IsSubgroup (s i)hs : β i: ?m.11633i, IsSubgroup: {G : Type ?u.11636} β [inst : Group G] β Set G β PropIsSubgroup (s: ΞΉ β Set Gs i: ?m.11633i)) (directed: β (i j : ΞΉ), β k, s i β s k β§ s j β s kdirected : β i: ?m.11669i j: ?m.11672j, β k: ?m.11678k, s: ΞΉ β Set Gs i: ?m.11669i β s: ΞΉ β Set Gs k: ?m.11678k β§ s: ΞΉ β Set Gs j: ?m.11672j β s: ΞΉ β Set Gs k: ?m.11678k) :
IsSubgroup: {G : Type ?u.11704} β [inst : Group G] β Set G β PropIsSubgroup (β i: ?m.11733i, s: ΞΉ β Set Gs i: ?m.11733i) :=
{ inv_mem := fun ha: ?m.12164ha =>
let β¨i: ΞΉi, hi: aβ β s ihiβ© := Set.mem_iUnion: β {Ξ± : Type ?u.12166} {ΞΉ : Sort ?u.12167} {x : Ξ±} {s : ΞΉ β Set Ξ±}, (x β iUnion fun i => s i) β β i, x β s iSet.mem_iUnion.1: β {a b : Prop}, (a β b) β a β b1 ha: ?m.12164ha
Set.mem_iUnion: β {Ξ± : Type ?u.12219} {ΞΉ : Sort ?u.12220} {x : Ξ±} {s : ΞΉ β Set Ξ±}, (x β iUnion fun i => s i) β β i, x β s iSet.mem_iUnion.2: β {a b : Prop}, (a β b) β b β a2 β¨i: ΞΉi, (hs: β (i : ΞΉ), IsSubgroup (s i)hs i: ΞΉi).inv_mem: β {G : Type ?u.12243} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem hi: aβ β s ihiβ©
toIsSubmonoid := isSubmonoid_iUnion_of_directed: β {M : Type ?u.11762} [inst : Monoid M] {ΞΉ : Type ?u.11761} [hΞΉ : Nonempty ΞΉ] {s : ΞΉ β Set M},
(β (i : ΞΉ), IsSubmonoid (s i)) β (β (i j : ΞΉ), β k, s i β s k β§ s j β s k) β IsSubmonoid (iUnion fun i => s i)isSubmonoid_iUnion_of_directed (fun i: ?m.11851i => (hs: β (i : ΞΉ), IsSubgroup (s i)hs i: ?m.11851i).toIsSubmonoid: β {G : Type ?u.11853} [inst : Group G] {s : Set G}, IsSubgroup s β IsSubmonoid stoIsSubmonoid) directed: β (i j : ΞΉ), β k, s i β s k β§ s j β s kdirected }
#align is_subgroup_Union_of_directed isSubgroup_iUnion_of_directed: β {G : Type u_2} [inst : Group G] {ΞΉ : Type u_1} [inst_1 : Nonempty ΞΉ] {s : ΞΉ β Set G},
(β (i : ΞΉ), IsSubgroup (s i)) β (β (i j : ΞΉ), β k, s i β s k β§ s j β s k) β IsSubgroup (iUnion fun i => s i)isSubgroup_iUnion_of_directed
#align is_add_subgroup_Union_of_directed isAddSubgroup_iUnion_of_directed: β {G : Type u_2} [inst : AddGroup G] {ΞΉ : Type u_1} [inst_1 : Nonempty ΞΉ] {s : ΞΉ β Set G},
(β (i : ΞΉ), IsAddSubgroup (s i)) β (β (i j : ΞΉ), β k, s i β s k β§ s j β s k) β IsAddSubgroup (iUnion fun i => s i)isAddSubgroup_iUnion_of_directed

end Group

namespace IsSubgroup

open IsSubmonoid

variable [Group: Type ?u.13019 β Type ?u.13019Group G: Type ?u.12512G] {s: Set Gs : Set: Type ?u.12478 β Type ?u.12478Set G: Type ?u.12512G} (hs: IsSubgroup shs : IsSubgroup: {G : Type ?u.12537} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs)

@[to_additive: β {G : Type u_1} {a : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β (-a β s β a β s)to_additive]
theorem inv_mem_iff: β {G : Type u_1} {a : G} [inst : Group G] {s : Set G}, IsSubgroup s β (aβ»ΒΉ β s β a β s)inv_mem_iff : a: Gaβ»ΒΉ β s: Set Gs β a: Ga β s: Set Gs :=
β¨fun h: ?m.12765h => byGoals accomplished! π G: Type u_1H: Type ?u.12515A: Type ?u.12518a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup sh: aβ»ΒΉ β sa β ssimpa using hs: IsSubgroup shs.inv_mem: β {G : Type ?u.12815} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem h: aβ»ΒΉ β shGoals accomplished! π, inv_mem: β {G : Type ?u.12771} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem hs: IsSubgroup shsβ©
#align is_subgroup.inv_mem_iff IsSubgroup.inv_mem_iff: β {G : Type u_1} {a : G} [inst : Group G] {s : Set G}, IsSubgroup s β (aβ»ΒΉ β s β a β s)IsSubgroup.inv_mem_iff
#align is_add_subgroup.neg_mem_iff IsAddSubgroup.neg_mem_iff: β {G : Type u_1} {a : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β (-a β s β a β s)IsAddSubgroup.neg_mem_iff

@[to_additive: β {G : Type u_1} {a b : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β a β s β (b + a β s β b β s)to_additive]
theorem mul_mem_cancel_right: a β s β (b * a β s β b β s)mul_mem_cancel_right (h: a β sh : a: Ga β s: Set Gs) : b: Gb * a: Ga β s: Set Gs β b: Gb β s: Set Gs :=
β¨fun hba: ?m.13872hba => byGoals accomplished! π G: Type u_1H: Type ?u.13003A: Type ?u.13006a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup sh: a β shba: b * a β sb β ssimpa using hs: IsSubgroup shs.mul_mem: β {M : Type ?u.14223} [inst : Monoid M] {s : Set M}, IsSubmonoid s β β {a b : M}, a β s β b β s β a * b β smul_mem hba: b * a β shba (hs: IsSubgroup shs.inv_mem: β {G : Type ?u.14229} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem h: a β sh)Goals accomplished! π, fun hb: ?m.13879hb => hs: IsSubgroup shs.mul_mem: β {M : Type ?u.13894} [inst : Monoid M] {s : Set M}, IsSubmonoid s β β {a b : M}, a β s β b β s β a * b β smul_mem hb: ?m.13879hb h: a β shβ©
#align is_subgroup.mul_mem_cancel_right IsSubgroup.mul_mem_cancel_right: β {G : Type u_1} {a b : G} [inst : Group G] {s : Set G}, IsSubgroup s β a β s β (b * a β s β b β s)IsSubgroup.mul_mem_cancel_right

@[to_additive: β {G : Type u_1} {a b : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s β a β s β (a + b β s β b β s)to_additive]
theorem mul_mem_cancel_left: a β s β (a * b β s β b β s)mul_mem_cancel_left (h: a β sh : a: Ga β s: Set Gs) : a: Ga * b: Gb β s: Set Gs β b: Gb β s: Set Gs :=
β¨fun hab: ?m.15379hab => byGoals accomplished! π G: Type u_1H: Type ?u.14510A: Type ?u.14513a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup sh: a β shab: a * b β sb β ssimpa using hs: IsSubgroup shs.mul_mem: β {M : Type ?u.15730} [inst : Monoid M] {s : Set M}, IsSubmonoid s β β {a b : M}, a β s β b β s β a * b β smul_mem (hs: IsSubgroup shs.inv_mem: β {G : Type ?u.15736} [inst : Group G] {s : Set G}, IsSubgroup s β β {a : G}, a β s β aβ»ΒΉ β sinv_mem h: a β sh) hab: a * b β shabGoals accomplished! π, hs: IsSubgroup shs.mul_mem: β {M : Type ?u.15398} [inst : Monoid M] {s : Set M}, IsSubmonoid s β β {a b : M}, a β s β b β s β a * b β smul_mem h: a β shβ©
#align is_subgroup.mul_mem_cancel_left IsSubgroup.mul_mem_cancel_left: β {G : Type u_1} {a b : G} [inst : Group G] {s : Set G}, IsSubgroup s β a β s β (a * b β s β b β s)IsSubgroup.mul_mem_cancel_left

end IsSubgroup

/-- `IsNormalAddSubgroup (s : Set A)` expresses the fact that `s` is a normal additive subgroup
of the additive group `A`. Important: the preferred way to say this in Lean is via bundled
subgroups `S : AddSubgroup A` and `hs : S.normal`, and not via this structure. -/
structure IsNormalAddSubgroup: {A : Type u_1} β [inst : AddGroup A] β Set A β PropIsNormalAddSubgroup [AddGroup: Type ?u.16114 β Type ?u.16114AddGroup A: Type ?u.16101A] (s: Set As : Set: Type ?u.16117 β Type ?u.16117Set A: Type ?u.16101A) extends IsAddSubgroup: {A : Type ?u.16121} β [inst : AddGroup A] β Set A β PropIsAddSubgroup s: Set As : Prop: TypeProp where
/-- The proposition that `s` is closed under (additive) conjugation. -/
normal: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s β β (n : A), n β s β β (g : A), g + n + -g β snormal : β n: ?m.16162n β s: Set As, β g: Ag : A: Type ?u.16101A, g: Ag + n: ?m.16162n + -g: Ag β s: Set As

/-- `IsNormalSubgroup (s : Set G)` expresses the fact that `s` is a normal subgroup
of the group `G`. Important: the preferred way to say this in Lean is via bundled
subgroups `S : Subgroup G` and not via this structure. -/
structure IsNormalSubgroup: β {G : Type u_1} [inst : Group G] {s : Set G},
IsSubgroup s β (β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β s) β IsNormalSubgroup sIsNormalSubgroup [Group: Type ?u.17311 β Type ?u.17311Group G: Type ?u.17292G] (s: Set Gs : Set: Type ?u.17314 β Type ?u.17314Set G: Type ?u.17292G) extends IsSubgroup: {G : Type ?u.17318} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs : Prop: TypeProp where
/-- The proposition that `s` is closed under conjugation. -/
normal: β {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β snormal : β n: ?m.17360n β s: Set Gs, β g: Gg : G: Type ?u.17292G, g: Gg * n: ?m.17360n * g: Ggβ»ΒΉ β s: Set Gs
#align is_normal_subgroup IsNormalSubgroup: {G : Type u_1} β [inst : Group G] β Set G β PropIsNormalSubgroup

theorem isNormalSubgroup_of_commGroup: β [inst : CommGroup G] {s : Set G}, IsSubgroup s β IsNormalSubgroup sisNormalSubgroup_of_commGroup [CommGroup: Type ?u.18689 β Type ?u.18689CommGroup G: Type ?u.18670G] {s: Set Gs : Set: Type ?u.18692 β Type ?u.18692Set G: Type ?u.18670G} (hs: IsSubgroup shs : IsSubgroup: {G : Type ?u.18695} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs) :
IsNormalSubgroup: {G : Type ?u.18736} β [inst : Group G] β Set G β PropIsNormalSubgroup s: Set Gs :=
{ hs: IsSubgroup shs with normal := fun n: ?m.18820n hn: ?m.18823hn g: ?m.18826g => byGoals accomplished! π G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gg * n * gβ»ΒΉ β srwa [G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gg * n * gβ»ΒΉ β smul_right_comm: β {G : Type ?u.18837} [inst : CommSemigroup G] (a b c : G), a * b * c = a * c * bmul_right_comm,G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gg * gβ»ΒΉ * n β s G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gg * n * gβ»ΒΉ β smul_right_inv: β {G : Type ?u.19122} [inst : Group G] (a : G), a * aβ»ΒΉ = 1mul_right_inv,G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: G1 * n β s G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gg * n * gβ»ΒΉ β sone_mul: β {M : Type ?u.19184} [inst : MulOneClass M] (a : M), 1 * a = aone_mulG: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gn β s]G: Type u_1H: Type ?u.18673A: Type ?u.18676a, aβ, aβ, b, c: Ginstβ: CommGroup Gs: Set Ghs: IsSubgroup sn: Ghn: n β sg: Gn β s }
#align is_normal_subgroup_of_comm_group isNormalSubgroup_of_commGroup: β {G : Type u_1} [inst : CommGroup G] {s : Set G}, IsSubgroup s β IsNormalSubgroup sisNormalSubgroup_of_commGroup

theorem Additive.isNormalAddSubgroup: β [inst : Group G] {s : Set G}, IsNormalSubgroup s β IsNormalAddSubgroup sAdditive.isNormalAddSubgroup [Group: Type ?u.19582 β Type ?u.19582Group G: Type ?u.19563G] {s: Set Gs : Set: Type ?u.19585 β Type ?u.19585Set G: Type ?u.19563G} (hs: IsNormalSubgroup shs : IsNormalSubgroup: {G : Type ?u.19588} β [inst : Group G] β Set G β PropIsNormalSubgroup s: Set Gs) :
@IsNormalAddSubgroup: {A : Type ?u.19619} β [inst : AddGroup A] β Set A β PropIsNormalAddSubgroup (Additive: Type ?u.19620 β Type ?u.19620Additive G: Type ?u.19563G) _ s: Set Gs :=
@IsNormalAddSubgroup.mk: β {A : Type ?u.19638} [inst : AddGroup A] {s : Set A},
(@IsNormalSubgroup.normal: β {G : Type ?u.19704} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β sIsNormalSubgroup.normal _: Type ?u.19704_ βΉGroup (Additive G)βΊ _: Set ?m.19705_ hs: IsNormalSubgroup shs)
-- porting note: Lean needs help synthesising

theorem Additive.isNormalAddSubgroup_iff: β {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalAddSubgroup s β IsNormalSubgroup sAdditive.isNormalAddSubgroup_iff [Group: Type ?u.20798 β Type ?u.20798Group G: Type ?u.20779G] {s: Set Gs : Set: Type ?u.20801 β Type ?u.20801Set G: Type ?u.20779G} :
@IsNormalAddSubgroup: {A : Type ?u.20804} β [inst : AddGroup A] β Set A β PropIsNormalAddSubgroup (Additive: Type ?u.20805 β Type ?u.20805Additive G: Type ?u.20779G) _ s: Set Gs β IsNormalSubgroup: {G : Type ?u.20822} β [inst : Group G] β Set G β PropIsNormalSubgroup s: Set Gs :=
IsSubgroup s β (β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β s) β IsNormalSubgroup sIsNormalSubgroup.mk G: Type u_1G _ _: Set G_ (Additive.isAddSubgroup_iff: β {G : Type ?u.20929} [inst : Group G] {s : Set G}, IsAddSubgroup s β IsSubgroup sAdditive.isAddSubgroup_iff.1: β {a b : Prop}, (a β b) β a β b1 hβ: IsAddSubgroup shβ) @hβ: β (n : Additive G), n β s β β (g : Additive G), g + n + -g β shβGoals accomplished! π,

theorem Multiplicative.isNormalSubgroup: β [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s β IsNormalSubgroup sMultiplicative.isNormalSubgroup [AddGroup: Type ?u.21006 β Type ?u.21006AddGroup A: Type ?u.20993A] {s: Set As : Set: Type ?u.21009 β Type ?u.21009Set A: Type ?u.20993A} (hs: IsNormalAddSubgroup shs : IsNormalAddSubgroup: {A : Type ?u.21012} β [inst : AddGroup A] β Set A β PropIsNormalAddSubgroup s: Set As) :
@IsNormalSubgroup: {G : Type ?u.21042} β [inst : Group G] β Set G β PropIsNormalSubgroup (Multiplicative: Type ?u.21043 β Type ?u.21043Multiplicative A: Type ?u.20993A) _ s: Set As :=
@IsNormalSubgroup.mk: β {G : Type ?u.21061} [inst : Group G] {s : Set G},
IsSubgroup s β (β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β s) β IsNormalSubgroup sIsNormalSubgroup.mk (Multiplicative: Type ?u.21062 β Type ?u.21062Multiplicative A: Type ?u.20993A) _ _: Set (Multiplicative A)_ (Multiplicative.isSubgroup: β {A : Type ?u.21082} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s β IsSubgroup sMultiplicative.isSubgroup hs: IsNormalAddSubgroup shs.toIsAddSubgroup: β {A : Type ?u.21111} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s β IsAddSubgroup stoIsAddSubgroup)
(@IsNormalAddSubgroup.normal: β {A : Type ?u.21126} [inst : AddGroup A] {s : Set A},
IsNormalAddSubgroup s β β (n : A), n β s β β (g : A), g + n + -g β sIsNormalAddSubgroup.normal _: Type ?u.21126_ βΉAddGroup (Multiplicative A)βΊ _: Set ?m.21127_ hs: IsNormalAddSubgroup shs)
#align multiplicative.is_normal_subgroup Multiplicative.isNormalSubgroup: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s β IsNormalSubgroup sMultiplicative.isNormalSubgroup

theorem Multiplicative.isNormalSubgroup_iff: β [inst : AddGroup A] {s : Set A}, IsNormalSubgroup s β IsNormalAddSubgroup sMultiplicative.isNormalSubgroup_iff [AddGroup: Type ?u.22220 β Type ?u.22220AddGroup A: Type ?u.22207A] {s: Set As : Set: Type ?u.22223 β Type ?u.22223Set A: Type ?u.22207A} :
@IsNormalSubgroup: {G : Type ?u.22226} β [inst : Group G] β Set G β PropIsNormalSubgroup (Multiplicative: Type ?u.22227 β Type ?u.22227Multiplicative A: Type ?u.22207A) _ s: Set As β IsNormalAddSubgroup: {A : Type ?u.22244} β [inst : AddGroup A] β Set A β PropIsNormalAddSubgroup s: Set As :=
β¨byGoals accomplished! π
G: Type ?u.22201H: Type ?u.22204A: Type u_1a, aβ, aβ, b, c: Ginstβ: AddGroup As: Set AIsNormalSubgroup s β IsNormalAddSubgroup srintro β¨hβ, hββ©: IsNormalSubgroup sβ¨hβ: IsSubgroup shββ¨hβ, hββ©: IsNormalSubgroup s, hβ: β (n : Multiplicative A), n β s β β (g : Multiplicative A), g * n * gβ»ΒΉ β shββ¨hβ, hββ©: IsNormalSubgroup sβ©G: Type ?u.22201H: Type ?u.22204A: Type u_1a, aβ, aβ, b, c: Ginstβ: AddGroup As: Set Ahβ: IsSubgroup shβ: β (n : Multiplicative A), n β s β β (g : Multiplicative A), g * n * gβ»ΒΉ β smkIsNormalAddSubgroup s;G: Type ?u.22201H: Type ?u.22204A: Type u_1a, aβ, aβ, b, c: Ginstβ: AddGroup As: Set Ahβ: IsSubgroup shβ: β (n : Multiplicative A), n β s β β (g : Multiplicative A), g * n * gβ»ΒΉ β smkIsNormalAddSubgroup s
G: Type ?u.22201H: Type ?u.22204A: Type u_1a, aβ, aβ, b, c: Ginstβ: AddGroup As: Set AIsNormalSubgroup s β IsNormalAddSubgroup sexact @IsNormalAddSubgroup.mk: β {A : Type ?u.22347} [inst : AddGroup A] {s : Set A},
IsAddSubgroup s β (β (n : A), n β s β β (g : A), g + n + -g β s) β IsNormalAddSubgroup sIsNormalAddSubgroup.mk A: Type u_1A _ _: Set A_ (Multiplicative.isSubgroup_iff: β {A : Type ?u.22351} [inst : AddGroup A] {s : Set A}, IsSubgroup s β IsAddSubgroup sMultiplicative.isSubgroup_iff.1: β {a b : Prop}, (a β b) β a β b1 hβ: IsSubgroup shβ) @hβ: β (n : Multiplicative A), n β s β β (g : Multiplicative A), g * n * gβ»ΒΉ β shβGoals accomplished! π,
fun h: ?m.22265h => Multiplicative.isNormalSubgroup: β {A : Type ?u.22267} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s β IsNormalSubgroup sMultiplicative.isNormalSubgroup h: ?m.22265hβ©
#align multiplicative.is_normal_subgroup_iff Multiplicative.isNormalSubgroup_iff: β {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsNormalSubgroup s β IsNormalAddSubgroup sMultiplicative.isNormalSubgroup_iff

namespace IsSubgroup

variable [Group: Type ?u.27820 β Type ?u.27820Group G: Type ?u.22407G]

-- Normal subgroup properties
@[to_additive: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsNormalAddSubgroup s β β {a b : G}, a + b β s β b + a β sto_additive]
theorem mem_norm_comm: β {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β smem_norm_comm {s: Set Gs : Set: Type ?u.22451 β Type ?u.22451Set G: Type ?u.22429G} (hs: IsNormalSubgroup shs : IsNormalSubgroup: {G : Type ?u.22454} β [inst : Group G] β Set G β PropIsNormalSubgroup s: Set Gs) {a: Ga b: Gb : G: Type ?u.22429G} (hab: a * b β shab : a: Ga * b: Gb β s: Set Gs) :
b: Gb * a: Ga β s: Set Gs := byGoals accomplished! π
G: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sb * a β shave h: aβ»ΒΉ * (a * b) * aβ»ΒΉβ»ΒΉ β sh : a: Gaβ»ΒΉ * (a: Ga * b: Gb) * a: Gaβ»ΒΉβ»ΒΉ β s: Set Gs := hs: IsNormalSubgroup shs.normal: β {G : Type ?u.25271} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β (n : G), n β s β β (g : G), g * n * gβ»ΒΉ β snormal (a: Ga * b: Gb) hab: a * b β shab a: Gaβ»ΒΉG: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sh: aβ»ΒΉ * (a * b) * aβ»ΒΉβ»ΒΉ β sb * a β s
G: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sb * a β ssimp at h: aβ»ΒΉ * (a * b) * aβ»ΒΉβ»ΒΉ β shG: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sh: b * a β sb * a β s;G: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sh: b * a β sb * a β s G: Type u_1H: Type ?u.22432A: Type ?u.22435aβ, aβ, aβ, bβ, c: Ginstβ: Group Gs: Set Ghs: IsNormalSubgroup sa, b: Ghab: a * b β sb * a β sexact h: b * a β shGoals accomplished! π
#align is_subgroup.mem_norm_comm IsSubgroup.mem_norm_comm: β {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β sIsSubgroup.mem_norm_comm
#align is_add_subgroup.mem_norm_comm IsAddSubgroup.mem_norm_comm: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsNormalAddSubgroup s β β {a b : G}, a + b β s β b + a β sIsAddSubgroup.mem_norm_comm

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsNormalAddSubgroup s β β {a b : G}, a + b β s β b + a β sto_additive]
theorem mem_norm_comm_iff: β {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β smem_norm_comm_iff {s: Set Gs : Set: Type ?u.26125 β Type ?u.26125Set G: Type ?u.26103G} (hs: IsNormalSubgroup shs : IsNormalSubgroup: {G : Type ?u.26128} β [inst : Group G] β Set G β PropIsNormalSubgroup s: Set Gs) {a: Ga b: Gb : G: Type ?u.26103G} : a: Ga * b: Gb β s: Set Gs β b: Gb * a: Ga β s: Set Gs :=
β¨mem_norm_comm: β {G : Type ?u.27295} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β smem_norm_comm hs: IsNormalSubgroup shs, mem_norm_comm: β {G : Type ?u.27328} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β smem_norm_comm hs: IsNormalSubgroup shsβ©
#align is_subgroup.mem_norm_comm_iff IsSubgroup.mem_norm_comm_iff: β {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s β β {a b : G}, a * b β s β b * a β sIsSubgroup.mem_norm_comm_iff
#align is_add_subgroup.mem_norm_comm_iff IsAddSubgroup.mem_norm_comm_iff: β {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsNormalAddSubgroup s β β {a b : G}, a + b β s β b + a β sIsAddSubgroup.mem_norm_comm_iff

/-- The trivial subgroup -/
def trivial: (G : Type ?u.27395) β [inst : Group G] β Set Gtrivial (G: Type ?u.27395G : Type _: Type (?u.27395+1)Type _) [Group: Type ?u.27398 β Type ?u.27398Group G: Type ?u.27395G] : Set: Type ?u.27401 β Type ?u.27401Set G: Type ?u.27395G :=
{1: ?m.274231}
#align is_subgroup.trivial IsSubgroup.trivial: (G : Type u_1) β [inst : Group G] β Set GIsSubgroup.trivial

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {g : G}, g β IsAddSubgroup.trivial G β g = 0to_additive (attr := simp)]
theorem mem_trivial: β {g : G}, g β trivial G β g = 1mem_trivial {g: Gg : G: Type ?u.27801G} : g: Gg β trivial: (G : Type ?u.27830) β [inst : Group G] β Set Gtrivial G: Type ?u.27801G β g: Gg = 1: ?m.278511 :=
mem_singleton_iff: β {Ξ± : Type ?u.28194} {a b : Ξ±}, a β {b} β a = bmem_singleton_iff
#align is_subgroup.mem_trivial IsSubgroup.mem_trivial: β {G : Type u_1} [inst : Group G] {g : G}, g β trivial G β g = 1IsSubgroup.mem_trivial

theorem trivial_normal: IsNormalSubgroup (trivial G)trivial_normal : IsNormalSubgroup: {G : Type ?u.28298} β [inst : Group G] β Set G β PropIsNormalSubgroup (trivial: (G : Type ?u.28320) β [inst : Group G] β Set Gtrivial G: Type ?u.28276G) := byGoals accomplished! π
G: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup (trivial G)refine' { .. }: IsNormalSubgroup ?m.28334{ .. }G: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_11 β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_2β {a b : G}, a β trivial G β b β trivial G β a * b β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_3β {a : G}, a β trivial G β aβ»ΒΉ β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_4β (n : G), n β trivial G β β (g : G), g * n * gβ»ΒΉ β trivial G G: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup (trivial G)<;>G: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_11 β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_2β {a b : G}, a β trivial G β b β trivial G β a * b β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_3β {a : G}, a β trivial G β aβ»ΒΉ β trivial GG: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group Grefine'_4β (n : G), n β trivial G β β (g : G), g * n * gβ»ΒΉ β trivial G G: Type u_1H: Type ?u.28279A: Type ?u.28282a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup (trivial G)simp (config := { contextual := true: Booltrue }) [trivial: (G : Type ?u.28748) β [inst : Group G] β Set Gtrivial]Goals accomplished! π
#align is_subgroup.trivial_normal IsSubgroup.trivial_normal: β {G : Type u_1} [inst : Group G], IsNormalSubgroup (trivial G)IsSubgroup.trivial_normal

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {s : Set G},
IsAddSubgroup s β (s = IsAddSubgroup.trivial G β β (x : G), x β s β x = 0)to_additive]
theorem eq_trivial_iff: β {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s β (s = trivial G β β (x : G), x β s β x = 1)eq_trivial_iff {s: Set Gs : Set: Type ?u.34570 β Type ?u.34570Set G: Type ?u.34548G} (hs: IsSubgroup shs : IsSubgroup: {G : Type ?u.34573} β [inst : Group G] β Set G β PropIsSubgroup s: Set Gs) : s: Set Gs = trivial: (G : Type ?u.34606) β [inst : Group G] β Set Gtrivial G: Type ?u.34548G β β x: ?m.34611x β s: Set Gs, x: ?m.34611x = (1: ?m.346521 : G: Type ?u.34548G) := byGoals accomplished! π
G: Type u_1H: Type ?u.34551A: Type ?u.34554a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup ss = trivial G β β (x : G), x β s β x = 1simp only [Set.ext_iff: β {Ξ± : Type ?u.34998} {s t : Set Ξ±}, s = t β β (x : Ξ±), x β s β x β tSet.ext_iff, IsSubgroup.mem_trivial: β {G : Type ?u.35016} [inst : Group G] {g : G}, g β trivial G β g = 1IsSubgroup.mem_trivial]G: Type u_1H: Type ?u.34551A: Type ?u.34554a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup s(β (x : G), x β s β x = 1) β β (x : G), x β s β x = 1;G: Type u_1H: Type ?u.34551A: Type ?u.34554a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup s(β (x : G), x β s β x = 1) β β (x : G), x β s β x = 1
G: Type u_1H: Type ?u.34551A: Type ?u.34554a, aβ, aβ, b, c: Ginstβ: Group Gs: Set Ghs: IsSubgroup ss = trivial G β β (x : G), x β s β x = 1exact β¨fun h: ?m.35168h x: ?m.35171x => (h: ?m.35168h x: ?m.35171x).1: β {a b : Prop}, (a β b) β a β b1, fun h: ?m.35182h x: ?m.35185x => β¨h: ?m.35182h x: ?m.35185x, fun hx: ?m.35197hx => hx: ?m.35197hx.symm: β {Ξ± : Sort ?u.35199} {a b : Ξ±}, a = b β b = asymm βΈ hs: IsSubgroup shs.toIsSubmonoid: β {G : Type ?u.35210} [inst : Group G] {s : Set G}, IsSubgroup s β IsSubmonoid stoIsSubmonoid.one_mem: β {M : Type ?u.35218} [inst : Monoid M] {s : Set M}, IsSubmonoid s β 1 β sone_memβ©β©Goals accomplished! π
#align is_subgroup.eq_trivial_iff IsSubgroup.eq_trivial_iff: β {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s β (s = trivial G β β (x : G), x β s β x = 1)IsSubgroup.eq_trivial_iff
IsAddSubgroup s β (s = IsAddSubgroup.trivial G β β (x : G), x β s β x = 0)IsAddSubgroup.eq_trivial_iff

theorem univ_subgroup: IsNormalSubgroup univuniv_subgroup : IsNormalSubgroup: {G : Type ?u.35615} β [inst : Group G] β Set G β PropIsNormalSubgroup (@univ: {Ξ± : Type ?u.35637} β Set Ξ±univ G: Type ?u.35593G) := byGoals accomplished! π G: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup univrefine' { .. }: IsNormalSubgroup ?m.35649{ .. }G: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_11 β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_2β {a b : G}, a β univ β b β univ β a * b β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_3β {a : G}, a β univ β aβ»ΒΉ β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_4β (n : G), n β univ β β (g : G), g * n * gβ»ΒΉ β univ G: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup univ<;>G: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_11 β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_2β {a b : G}, a β univ β b β univ β a * b β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_3β {a : G}, a β univ β aβ»ΒΉ β univG: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group Grefine'_4β (n : G), n β univ β β (g : G), g * n * gβ»ΒΉ β univ G: Type u_1H: Type ?u.35596A: Type ?u.35599a, aβ, aβ, b, c: Ginstβ: Group GIsNormalSubgroup univsimpGoals accomplished! π
#align is_subgroup.univ_subgroup IsSubgroup.univ_subgroup: β {G : Type u_1} [inst : Group G], IsNormalSubgroup univIsSubgroup.univ_subgroup

/-- The underlying set of the center of a group. -/
def center: (G : Type u_1) β [inst : Group G] β Set Gcenter (G: Type ?u.38576G : Type _: Type (?u.38576+1)Type _) [Group: Type ?u.38579 β Type ?u.38579Group G: Type ?u.38576G] : Set: Type ?u.38582 β Type ?u.38582Set G: Type ?u.38576G :=
{ z: ?m.38593z | β g: ?m.38596g, g: ?m.38596g * z: ?m.38593z = z: ?m.38593z * g: ?m.38596g }
#align is_subgroup.center IsSubgroup.center: (G : Type u_1) β [inst : Group G] β Set GIsSubgroup.center

theorem mem_center: β {a : G}, a β center G β β (g : G), g * a = a * gmem_center {a: Ga : G: Type ?u.39733G} : a: Ga β center: (G : Type ?u.39762) β [inst : Group G] β Set Gcenter G: Type ?u.39733G β β g: ?m.39782g, g: ?m.39782g * a: Ga = a: Ga * g: ?m.39782g :=
Iff.rfl: β {a : Prop}, a β aIff.rfl
#align is_subgroup.mem_center IsSubgroup.mem_center: β {G : Type u_1} [inst : Group G] {a : G}, a β center G β β (g : G), g * a = a * gIsSubgroup.mem_center

theorem center_normal: β {G : Type u_1} [inst : Group G], IsNormalSubgroup (center G)center_normal : IsNormalSubgroup: {G : Type ?u.40930} β [inst : Group G] β Set G β PropIsNormalSubgroup (center: (G : Type ?u.40952) β [inst : Group G] β Set Gcenter G: Type ?u.40908G) :=
{ one_mem := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group G1 β center Gsimp [center: (G : Type ?u.47115) β [inst : Group G] β Set Gcenter]Goals accomplished! π
mul_mem := fun ha: ?m.41278ha hb: ?m.41281hb g: ?m.41284g => byGoals accomplished! π
G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * grw [G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * gβ mul_assoc: β {G : Type ?u.49232} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * aβ * bβ = aβ * bβ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * gmem_center: β {G : Type ?u.49551} [inst : Group G] {a : G}, a β center G β β (g : G), g * a = a * gmem_center.2: β {a b : Prop}, (a β b) β b β a2 ha: aβ β center Gha g: Gg,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gaβ * g * bβ = aβ * bβ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * gmul_assoc: β {G : Type ?u.49592} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gaβ * (g * bβ) = aβ * bβ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * gmem_center: β {G : Type ?u.49649} [inst : Group G] {a : G}, a β center G β β (g : G), g * a = a * gmem_center.2: β {a b : Prop}, (a β b) β b β a2 hb: bβ β center Ghb g: Gg,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gaβ * (bβ * g) = aβ * bβ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gg * (aβ * bβ) = aβ * bβ * gβ mul_assoc: β {G : Type ?u.49680} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocG: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gaβ, bβ: Gha: aβ β center Ghb: bβ β center Gg: Gaβ * bβ * g = aβ * bβ * g]Goals accomplished! π
inv_mem := fun {a: ?m.41304a} ha: ?m.41307ha g: ?m.41310g =>
calc
g: ?m.41310g * a: ?m.41304aβ»ΒΉ = a: ?m.41304aβ»ΒΉ * (g: ?m.41310g * a: ?m.41304a) * a: ?m.41304aβ»ΒΉ := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gg * aβ»ΒΉ = aβ»ΒΉ * (g * a) * aβ»ΒΉsimp [ha: a β center Gha g: Gg]Goals accomplished! π
_: ?mβ_ = a: ?m.41304aβ»ΒΉ * g: ?m.41310g := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * (g * a) * aβ»ΒΉ = aβ»ΒΉ * grw [G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * (g * a) * aβ»ΒΉ = aβ»ΒΉ * gβ mul_assoc: β {G : Type ?u.50189} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * g * a * aβ»ΒΉ = aβ»ΒΉ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * (g * a) * aβ»ΒΉ = aβ»ΒΉ * gmul_assoc: β {G : Type ?u.50252} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocG: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * g * (a * aβ»ΒΉ) = aβ»ΒΉ * g]G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * g * (a * aβ»ΒΉ) = aβ»ΒΉ * g;G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * g * (a * aβ»ΒΉ) = aβ»ΒΉ * g G: Type u_1H: Type ?u.40911A: Type ?u.40914aβ, aβ, aβ, b, c: Ginstβ: Group Ga: Gha: a β center Gg: Gaβ»ΒΉ * (g * a) * aβ»ΒΉ = aβ»ΒΉ * gsimpGoals accomplished! π
normal := fun n: ?m.43573n ha: ?m.43576ha g: ?m.43579g h: ?m.43582h =>
calc
h: ?m.43582h * (g: ?m.43579g * n: ?m.43573n * g: ?m.43579gβ»ΒΉ) = h: ?m.43582h * n: ?m.43573n := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gh * (g * n * gβ»ΒΉ) = h * nsimp [ha: n β center Gha g: Gg, mul_assoc: β {G : Type ?u.50817} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! π
_: ?mβ_ = g: ?m.43579g * g: ?m.43579gβ»ΒΉ * n: ?m.43573n * h: ?m.43582h := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gh * n = g * gβ»ΒΉ * n * hrw [G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gh * n = g * gβ»ΒΉ * n * hha: n β center Gha h: GhG: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gn * h = g * gβ»ΒΉ * n * h]G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gn * h = g * gβ»ΒΉ * n * h;G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gn * h = g * gβ»ΒΉ * n * h G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gh * n = g * gβ»ΒΉ * n * hsimpGoals accomplished! π
_: ?mβ_ = g: ?m.43579g * n: ?m.43573n * g: ?m.43579gβ»ΒΉ * h: ?m.43582h := byGoals accomplished! π G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * gβ»ΒΉ * n * h = g * n * gβ»ΒΉ * hrw [G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * gβ»ΒΉ * n * h = g * n * gβ»ΒΉ * hmul_assoc: β {G : Type ?u.50979} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc g: Gg,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * (gβ»ΒΉ * n) * h = g * n * gβ»ΒΉ * h G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * gβ»ΒΉ * n * h = g * n * gβ»ΒΉ * hha: n β center Gha g: Ggβ»ΒΉ,G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * (n * gβ»ΒΉ) * h = g * n * gβ»ΒΉ * h G: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * gβ»ΒΉ * n * h = g * n * gβ»ΒΉ * hβ mul_assoc: β {G : Type ?u.51031} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocG: Type u_1H: Type ?u.40911A: Type ?u.40914a, aβ, aβ, b, c: Ginstβ: Group Gn: Gha: n β center Gg, h: Gg * n * gβ»ΒΉ * h = g * n * gβ»ΒΉ * h]Goals accomplished! π
}
#align is_subgroup.center_normal IsSubgroup.center_normal: β {G : Type u_1} [inst : Group G], IsNormalSubgroup (center G)IsSubgroup.center_normal

/-- The underlying set of the normalizer of a subset `S : Set G` of a group `G`. That is,
the elements `g : G` such that `g * S * gβ»ΒΉ = S`. -/
"The underlying set of the normalizer of a subset `S : Set A` of an
additive group `A`. That is, the elements `a : A` such that `a + S - a = S`."]
def normalizer: {G : Type u_1} β [inst : Group G] β Set G β Set Gnormalizer (s: Set Gs : Set: Type ?u.51199 β Type ?u.51199Set G: Type ?u.51177G) : Set: Type ?u.51202 β Type ?u.51202Set G: Type ?u.51177G :=
{ g: Gg : G: Type ?u.51177G | β n: ?m.51213n, n: ?m.51213n β s: Set Gs β g: Gg * n: ?m.51213n * g: Ggβ»ΒΉ β s: Set Gs }
#align is_subgroup.normalizer IsSubgroup.normalizer: {G : Type u_1} β [inst : Group G] β Set G β Set GIsSubgroup.normalizer