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.
/-
Copyright (c) 2018 Johannes Hรถlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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,
please use `Subgroup G` and `AddSubgroup A`, defined in `GroupTheory.Subgroup.Basic`.

## 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.77632
G
:
Type _: Type (?u.39733+1)
Type _
} {
H: Type ?u.5
H
:
Type _: Type (?u.5+1)
Type _
} {
A: Type ?u.77638
A
:
Type _: Type (?u.8+1)
Type _
} {
a: G
a
aโ‚: G
aโ‚
aโ‚‚: G
aโ‚‚
b: G
b
c: G
c
:
G: Type ?u.77632
G
} section Group variable [
Group: Type ?u.65 โ†’ Type ?u.65
Group
G: Type ?u.21
G
] [
AddGroup: Type ?u.68 โ†’ Type ?u.68
AddGroup
A: Type ?u.2675
A
] /-- `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 s
IsAddSubgroup
(
s: Set A
s
:
Set: Type ?u.71 โ†’ Type ?u.71
Set
A: Type ?u.52
A
) extends
IsAddSubmonoid: {A : Type ?u.75} โ†’ [inst : AddMonoid A] โ†’ Set A โ†’ Prop
IsAddSubmonoid
s: Set A
s
:
Prop: Type
Prop
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 โˆˆ s
neg_mem
{
a: ?m.371
a
} :
a: ?m.371
a
โˆˆ
s: Set A
s
โ†’ -
a: ?m.371
a
โˆˆ
s: Set A
s
#align is_add_subgroup
IsAddSubgroup: {A : Type u_1} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
/-- `s` is a subgroup: a set containing 1 and closed under multiplication and inverse. -/ @[
to_additive: {A : Type u_1} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
to_additive
] structure
IsSubgroup: {G : Type u_1} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
s: Set G
s
:
Set: Type ?u.660 โ†’ Type ?u.660
Set
G: Type ?u.635
G
) extends
IsSubmonoid: {M : Type ?u.664} โ†’ [inst : Monoid M] โ†’ Set M โ†’ Prop
IsSubmonoid
s: Set G
s
:
Prop: Type
Prop
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โปยน โˆˆ s
inv_mem
{
a: ?m.990
a
} :
a: ?m.990
a
โˆˆ
s: Set G
s
โ†’
a: ?m.990
a
โปยน โˆˆ
s: Set G
s
#align is_subgroup
IsSubgroup: {G : Type u_1} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s โ†’ โˆ€ {x y : G}, x โˆˆ s โ†’ y โˆˆ s โ†’ x - y โˆˆ s
to_additive
] theorem
IsSubgroup.div_mem: โˆ€ {s : Set G}, IsSubgroup s โ†’ โˆ€ {x y : G}, x โˆˆ s โ†’ y โˆˆ s โ†’ x / y โˆˆ s
IsSubgroup.div_mem
{
s: Set G
s
:
Set: Type ?u.1266 โ†’ Type ?u.1266
Set
G: Type ?u.1241
G
} (hs :
IsSubgroup: {G : Type ?u.1269} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
) {
x: G
x
y: G
y
:
G: Type ?u.1241
G
} (
hx: x โˆˆ s
hx
:
x: G
x
โˆˆ
s: Set G
s
) (
hy: y โˆˆ s
hy
:
y: G
y
โˆˆ
s: Set G
s
) :
x: G
x
/
y: G
y
โˆˆ
s: Set G
s
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.1244

A: Type ?u.1247

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

hs: IsSubgroup s

x, y: G

hx: x โˆˆ s

hy: y โˆˆ s


x / y โˆˆ s

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 โˆˆ s
IsSubgroup.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 โˆˆ s
IsAddSubgroup.sub_mem
theorem
Additive.isAddSubgroup: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsAddSubgroup s
Additive.isAddSubgroup
{
s: Set G
s
:
Set: Type ?u.2212 โ†’ Type ?u.2212
Set
G: Type ?u.2187
G
} (hs :
IsSubgroup: {G : Type ?u.2215} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
) : @
IsAddSubgroup: {A : Type ?u.2246} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
(
Additive: Type ?u.2247 โ†’ Type ?u.2247
Additive
G: Type ?u.2187
G
) _
s: Set G
s
:= @
IsAddSubgroup.mk: โˆ€ {A : Type ?u.2264} [inst : AddGroup A] {s : Set A}, IsAddSubmonoid s โ†’ (โˆ€ {a : A}, a โˆˆ s โ†’ -a โˆˆ s) โ†’ IsAddSubgroup s
IsAddSubgroup.mk
(
Additive: Type ?u.2265 โ†’ Type ?u.2265
Additive
G: Type ?u.2187
G
) _
_: Set (Additive G)
_
(
Additive.isAddSubmonoid: โˆ€ {M : Type ?u.2286} [inst : Monoid M] {s : Set M}, IsSubmonoid s โ†’ IsAddSubmonoid s
Additive.isAddSubmonoid
hs.
toIsSubmonoid: โˆ€ {G : Type ?u.2344} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsSubmonoid s
toIsSubmonoid
) hs.
inv_mem: โˆ€ {G : Type ?u.2640} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
#align additive.is_add_subgroup
Additive.isAddSubgroup: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsAddSubgroup s
Additive.isAddSubgroup
theorem
Additive.isAddSubgroup_iff: โˆ€ {s : Set G}, IsAddSubgroup s โ†” IsSubgroup s
Additive.isAddSubgroup_iff
{
s: Set G
s
:
Set: Type ?u.2694 โ†’ Type ?u.2694
Set
G: Type ?u.2669
G
} : @
IsAddSubgroup: {A : Type ?u.2697} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
(
Additive: Type ?u.2698 โ†’ Type ?u.2698
Additive
G: Type ?u.2669
G
) _
s: Set G
s
โ†”
IsSubgroup: {G : Type ?u.2715} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
:= โŸจ

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.2672

A: Type ?u.2675

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G


G: Type u_1

H: Type ?u.2672

A: Type ?u.2675

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

hโ‚ƒ: โˆ€ {a : Additive G}, a โˆˆ s โ†’ -a โˆˆ s

hโ‚: 0 โˆˆ s

hโ‚‚: โˆ€ {a b : Additive G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s


mk.mk
G: Type u_1

H: Type ?u.2672

A: Type ?u.2675

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

hโ‚ƒ: โˆ€ {a : Additive G}, a โˆˆ s โ†’ -a โˆˆ s

hโ‚: 0 โˆˆ s

hโ‚‚: โˆ€ {a b : Additive G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s


mk.mk
G: Type u_1

H: Type ?u.2672

A: Type ?u.2675

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G



Goals accomplished! ๐Ÿ™
, fun
h: ?m.2734
h
=>
Additive.isAddSubgroup: โˆ€ {G : Type ?u.2736} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsAddSubgroup s
Additive.isAddSubgroup
h: ?m.2734
h
โŸฉ #align additive.is_add_subgroup_iff
Additive.isAddSubgroup_iff: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsAddSubgroup s โ†” IsSubgroup s
Additive.isAddSubgroup_iff
theorem
Multiplicative.isSubgroup: โˆ€ {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ IsSubgroup s
Multiplicative.isSubgroup
{
s: Set A
s
:
Set: Type ?u.3254 โ†’ Type ?u.3254
Set
A: Type ?u.3235
A
} (hs :
IsAddSubgroup: {A : Type ?u.3257} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
s: Set A
s
) : @
IsSubgroup: {G : Type ?u.3287} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
Multiplicative: Type ?u.3288 โ†’ Type ?u.3288
Multiplicative
A: Type ?u.3235
A
) _
s: Set A
s
:= @
IsSubgroup.mk: โˆ€ {G : Type ?u.3305} [inst : Group G] {s : Set G}, IsSubmonoid s โ†’ (โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s) โ†’ IsSubgroup s
IsSubgroup.mk
(
Multiplicative: Type ?u.3306 โ†’ Type ?u.3306
Multiplicative
A: Type ?u.3235
A
) _ _ (
Multiplicative.isSubmonoid: โˆ€ {A : Type ?u.3327} [inst : AddMonoid A] {s : Set A}, IsAddSubmonoid s โ†’ IsSubmonoid s
Multiplicative.isSubmonoid
hs.
toIsAddSubmonoid: โˆ€ {A : Type ?u.3382} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ IsAddSubmonoid s
toIsAddSubmonoid
) hs.
neg_mem: โˆ€ {A : Type ?u.3652} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ โˆ€ {a : A}, a โˆˆ s โ†’ -a โˆˆ s
neg_mem
#align multiplicative.is_subgroup
Multiplicative.isSubgroup: โˆ€ {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ IsSubgroup s
Multiplicative.isSubgroup
theorem
Multiplicative.isSubgroup_iff: โˆ€ {s : Set A}, IsSubgroup s โ†” IsAddSubgroup s
Multiplicative.isSubgroup_iff
{
s: Set A
s
:
Set: Type ?u.3706 โ†’ Type ?u.3706
Set
A: Type ?u.3687
A
} : @
IsSubgroup: {G : Type ?u.3709} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
Multiplicative: Type ?u.3710 โ†’ Type ?u.3710
Multiplicative
A: Type ?u.3687
A
) _
s: Set A
s
โ†”
IsAddSubgroup: {A : Type ?u.3727} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
s: Set A
s
:= โŸจ

Goals accomplished! ๐Ÿ™
G: Type ?u.3681

H: Type ?u.3684

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set A


G: Type ?u.3681

H: Type ?u.3684

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set A

hโ‚ƒ: โˆ€ {a : Multiplicative A}, a โˆˆ s โ†’ aโปยน โˆˆ s

hโ‚: 1 โˆˆ s

hโ‚‚: โˆ€ {a b : Multiplicative A}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s


mk.mk
G: Type ?u.3681

H: Type ?u.3684

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set A

hโ‚ƒ: โˆ€ {a : Multiplicative A}, a โˆˆ s โ†’ aโปยน โˆˆ s

hโ‚: 1 โˆˆ s

hโ‚‚: โˆ€ {a b : Multiplicative A}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s


mk.mk
G: Type ?u.3681

H: Type ?u.3684

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set A



Goals accomplished! ๐Ÿ™
, fun
h: ?m.3747
h
=>
Multiplicative.isSubgroup: โˆ€ {A : Type ?u.3749} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ IsSubgroup s
Multiplicative.isSubgroup
h: ?m.3747
h
โŸฉ #align multiplicative.is_subgroup_iff
Multiplicative.isSubgroup_iff: โˆ€ {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsSubgroup s โ†” IsAddSubgroup s
Multiplicative.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 s
of_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 s
IsSubgroup.of_div
(
s: Set G
s
:
Set: Type ?u.4236 โ†’ Type ?u.4236
Set
G: Type ?u.4211
G
) (
one_mem: 1 โˆˆ s
one_mem
: (
1: ?m.4260
1
:
G: Type ?u.4211
G
) โˆˆ
s: Set G
s
) (
div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s
div_mem
: โˆ€ {
a: G
a
b: G
b
:
G: Type ?u.4211
G
},
a: G
a
โˆˆ
s: Set G
s
โ†’
b: G
b
โˆˆ
s: Set G
s
โ†’
a: G
a
*
b: G
b
โปยน โˆˆ
s: Set G
s
) :
IsSubgroup: {G : Type ?u.5484} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
:= have
inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
: โˆ€
a: ?m.5520
a
,
a: ?m.5520
a
โˆˆ
s: Set G
s
โ†’
a: ?m.5520
a
โปยน โˆˆ
s: Set G
s
:= fun
a: ?m.5750
a
ha: ?m.5753
ha
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s


G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s

this: 1 * aโปยน โˆˆ s


G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s


G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s

this: 1 * aโปยน โˆˆ s


h.e'_4
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s


G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s

this: 1 * aโปยน โˆˆ s


h.e'_4
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

a: G

ha: a โˆˆ s

this: 1 * aโปยน โˆˆ s


h.e'_4

Goals accomplished! ๐Ÿ™
{ inv_mem :=
inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
_: G
_
mul_mem := fun {
a: ?m.6056
a
b: ?m.6059
b
}
ha: ?m.6062
ha
hb: ?m.6065
hb
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s


a * b โˆˆ s
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s

this: a * bโปยนโปยน โˆˆ s


a * b โˆˆ s
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s


a * b โˆˆ s
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s

this: a * bโปยนโปยน โˆˆ s


h.e'_4.h.e'_6
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s


a * b โˆˆ s
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s

this: a * bโปยนโปยน โˆˆ s


h.e'_4.h.e'_6
G: Type u_1

H: Type ?u.4214

A: Type ?u.4217

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set G

one_mem: 1 โˆˆ s

div_mem: โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * bโปยน โˆˆ s

inv_mem: โˆ€ (a : G), a โˆˆ s โ†’ aโปยน โˆˆ s

a, b: G

ha: a โˆˆ s

hb: b โˆˆ s

this: a * bโปยนโปยน โˆˆ s


h.e'_4.h.e'_6
b = b

Goals accomplished! ๐Ÿ™
one_mem: 1 โˆˆ s
one_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 s
IsSubgroup.of_div
#align is_add_subgroup.of_add_neg
IsAddSubgroup.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 s
IsAddSubgroup.of_add_neg
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 s
IsAddSubgroup.of_sub
(
s: Set A
s
:
Set: Type ?u.9272 โ†’ Type ?u.9272
Set
A: Type ?u.9253
A
) (
zero_mem: 0 โˆˆ s
zero_mem
: (
0: ?m.9296
0
:
A: Type ?u.9253
A
) โˆˆ
s: Set A
s
) (
sub_mem: โˆ€ {a b : A}, a โˆˆ s โ†’ b โˆˆ s โ†’ a - b โˆˆ s
sub_mem
: โˆ€ {
a: A
a
b: A
b
:
A: Type ?u.9253
A
},
a: A
a
โˆˆ
s: Set A
s
โ†’
b: A
b
โˆˆ
s: Set A
s
โ†’
a: A
a
-
b: A
b
โˆˆ
s: Set A
s
) :
IsAddSubgroup: {A : Type ?u.10053} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
s: Set A
s
:=
IsAddSubgroup.of_add_neg: โˆ€ {G : Type ?u.10086} [inst : AddGroup G] (s : Set G), 0 โˆˆ s โ†’ (โˆ€ {a b : G}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + -b โˆˆ s) โ†’ IsAddSubgroup s
IsAddSubgroup.of_add_neg
s: Set A
s
zero_mem: 0 โˆˆ s
zero_mem
fun {
x: ?m.10102
x
y: ?m.10105
y
}
hx: ?m.10108
hx
hy: ?m.10111
hy
=>

Goals accomplished! ๐Ÿ™
G: Type ?u.9247

H: Type ?u.9250

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœยน: Group G

instโœ: AddGroup A

s: Set A

zero_mem: 0 โˆˆ s

sub_mem: โˆ€ {a b : A}, a โˆˆ s โ†’ b โˆˆ s โ†’ a - b โˆˆ s

x, y: A

hx: x โˆˆ s

hy: y โˆˆ s


x + -y โˆˆ s

Goals 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 s
IsAddSubgroup.of_sub
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] {sโ‚ sโ‚‚ : Set G}, IsAddSubgroup sโ‚ โ†’ IsAddSubgroup sโ‚‚ โ†’ IsAddSubgroup (sโ‚ โˆฉ sโ‚‚)
to_additive
] 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 G
sโ‚
sโ‚‚: Set G
sโ‚‚
:
Set: Type ?u.10386 โ†’ Type ?u.10386
Set
G: Type ?u.10358
G
} (
hsโ‚: IsSubgroup sโ‚
hsโ‚
:
IsSubgroup: {G : Type ?u.10389} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
sโ‚: Set G
sโ‚
) (
hsโ‚‚: IsSubgroup sโ‚‚
hsโ‚‚
:
IsSubgroup: {G : Type ?u.10420} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
sโ‚‚: Set G
sโ‚‚
) :
IsSubgroup: {G : Type ?u.10446} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
sโ‚: Set G
sโ‚
โˆฉ
sโ‚‚: Set G
sโ‚‚
) := {
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 s
toIsSubmonoid
hsโ‚‚: IsSubgroup sโ‚‚
hsโ‚‚
.
toIsSubmonoid: โˆ€ {G : Type ?u.10549} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsSubmonoid s
toIsSubmonoid
with inv_mem := fun
hx: ?m.10875
hx
=> โŸจ
hsโ‚: IsSubgroup sโ‚
hsโ‚
.
inv_mem: โˆ€ {G : Type ?u.10885} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
hx: ?m.10875
hx
.
1: โˆ€ {a b : Prop}, a โˆง b โ†’ a
1
,
hsโ‚‚: IsSubgroup sโ‚‚
hsโ‚‚
.
inv_mem: โˆ€ {G : Type ?u.10895} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
hx: ?m.10875
hx
.
2: โˆ€ {a b : Prop}, a โˆง b โ†’ b
2
โŸฉ } #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
#align is_add_subgroup.inter
IsAddSubgroup.inter: โˆ€ {G : Type u_1} [inst : AddGroup G] {sโ‚ sโ‚‚ : Set G}, IsAddSubgroup sโ‚ โ†’ IsAddSubgroup sโ‚‚ โ†’ IsAddSubgroup (sโ‚ โˆฉ sโ‚‚)
IsAddSubgroup.inter
@[
to_additive: โˆ€ {G : Type u_2} [inst : AddGroup G] {ฮน : Sort u_1} {s : ฮน โ†’ Set G}, (โˆ€ (y : ฮน), IsAddSubgroup (s y)) โ†’ IsAddSubgroup (Set.iInter s)
to_additive
] 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.10978
Sort
Sort _: Type ?u.10978
_
} {
s: ฮน โ†’ Set G
s
:
ฮน: Sort ?u.10978
ฮน
โ†’
Set: Type ?u.10983 โ†’ Type ?u.10983
Set
G: Type ?u.10953
G
} (
hs: โˆ€ (y : ฮน), IsSubgroup (s y)
hs
: โˆ€
y: ฮน
y
:
ฮน: Sort ?u.10978
ฮน
,
IsSubgroup: {G : Type ?u.10990} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
s: ฮน โ†’ Set G
s
y: ฮน
y
)) :
IsSubgroup: {G : Type ?u.11022} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
Set.iInter: {ฮฒ : Type ?u.11045} โ†’ {ฮน : Sort ?u.11044} โ†’ (ฮน โ†’ Set ฮฒ) โ†’ Set ฮฒ
Set.iInter
s: ฮน โ†’ Set G
s
) := {
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.11097
y
=> (
hs: โˆ€ (y : ฮน), IsSubgroup (s y)
hs
y: ?m.11097
y
).
toIsSubmonoid: โˆ€ {G : Type ?u.11099} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsSubmonoid s
toIsSubmonoid
with inv_mem := fun
h: ?m.11461
h
=>
Set.mem_iInter: โˆ€ {ฮฑ : Type ?u.11463} {ฮน : Sort ?u.11464} {x : ฮฑ} {s : ฮน โ†’ Set ฮฑ}, (x โˆˆ Set.iInter fun i => s i) โ†” โˆ€ (i : ฮน), x โˆˆ s i
Set.mem_iInter
.
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
fun
y: ?m.11481
y
=>
IsSubgroup.inv_mem: โˆ€ {G : Type ?u.11483} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s
IsSubgroup.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 i
Set.mem_iInter
.
1: โˆ€ {a b : Prop}, (a โ†” b) โ†’ a โ†’ b
1
h: ?m.11461
h
y: ?m.11481
y
) } #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}, (โˆ€ (y : ฮน), IsAddSubgroup (s y)) โ†’ IsAddSubgroup (iInter s)
IsAddSubgroup.iInter
@[
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 โ†’ Prop
Nonempty
ฮน: Type ?u.11620
ฮน
] {
s: ฮน โ†’ Set G
s
:
ฮน: Type ?u.11620
ฮน
โ†’
Set: Type ?u.11628 โ†’ Type ?u.11628
Set
G: Type ?u.11595
G
} (
hs: โˆ€ (i : ฮน), IsSubgroup (s i)
hs
: โˆ€
i: ?m.11633
i
,
IsSubgroup: {G : Type ?u.11636} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
s: ฮน โ†’ Set G
s
i: ?m.11633
i
)) (
directed: โˆ€ (i j : ฮน), โˆƒ k, s i โŠ† s k โˆง s j โŠ† s k
directed
: โˆ€
i: ?m.11669
i
j: ?m.11672
j
, โˆƒ
k: ?m.11678
k
,
s: ฮน โ†’ Set G
s
i: ?m.11669
i
โŠ†
s: ฮน โ†’ Set G
s
k: ?m.11678
k
โˆง
s: ฮน โ†’ Set G
s
j: ?m.11672
j
โŠ†
s: ฮน โ†’ Set G
s
k: ?m.11678
k
) :
IsSubgroup: {G : Type ?u.11704} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(โ‹ƒ
i: ?m.11733
i
,
s: ฮน โ†’ Set G
s
i: ?m.11733
i
) := { inv_mem := fun
ha: ?m.12164
ha
=> let โŸจ
i: ฮน
i
,
hi: aโœ โˆˆ s i
hi
โŸฉ :=
Set.mem_iUnion: โˆ€ {ฮฑ : Type ?u.12166} {ฮน : Sort ?u.12167} {x : ฮฑ} {s : ฮน โ†’ Set ฮฑ}, (x โˆˆ iUnion fun i => s i) โ†” โˆƒ i, x โˆˆ s i
Set.mem_iUnion
.
1: โˆ€ {a b : Prop}, (a โ†” b) โ†’ a โ†’ b
1
ha: ?m.12164
ha
Set.mem_iUnion: โˆ€ {ฮฑ : Type ?u.12219} {ฮน : Sort ?u.12220} {x : ฮฑ} {s : ฮน โ†’ Set ฮฑ}, (x โˆˆ iUnion fun i => s i) โ†” โˆƒ i, x โˆˆ s i
Set.mem_iUnion
.
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
โŸจ
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โปยน โˆˆ s
inv_mem
hi: aโœ โˆˆ s i
hi
โŸฉ 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.11851
i
=> (
hs: โˆ€ (i : ฮน), IsSubgroup (s i)
hs
i: ?m.11851
i
).
toIsSubmonoid: โˆ€ {G : Type ?u.11853} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsSubmonoid s
toIsSubmonoid
)
directed: โˆ€ (i j : ฮน), โˆƒ k, s i โŠ† s k โˆง s j โŠ† s k
directed
} #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.13019
Group
G: Type ?u.12512
G
] {
s: Set G
s
:
Set: Type ?u.12478 โ†’ Type ?u.12478
Set
G: Type ?u.12512
G
} (hs :
IsSubgroup: {G : Type ?u.12537} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
) @[
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: G
a
โปยน โˆˆ
s: Set G
s
โ†”
a: G
a
โˆˆ
s: Set G
s
:= โŸจfun
h: ?m.12765
h
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.12515

A: Type ?u.12518

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s

h: aโปยน โˆˆ s



Goals accomplished! ๐Ÿ™
,
inv_mem: โˆ€ {G : Type ?u.12771} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ โˆ€ {a : G}, a โˆˆ s โ†’ aโปยน โˆˆ s
inv_mem
hsโŸฉ #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 โˆˆ s
h
:
a: G
a
โˆˆ
s: Set G
s
) :
b: G
b
*
a: G
a
โˆˆ
s: Set G
s
โ†”
b: G
b
โˆˆ
s: Set G
s
:= โŸจfun
hba: ?m.13872
hba
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.13003

A: Type ?u.13006

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s

h: a โˆˆ s

hba: b * a โˆˆ s



Goals accomplished! ๐Ÿ™
, fun
hb: ?m.13879
hb
=> hs.
mul_mem: โˆ€ {M : Type ?u.13894} [inst : Monoid M] {s : Set M}, IsSubmonoid s โ†’ โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
mul_mem
hb: ?m.13879
hb
h: a โˆˆ s
h
โŸฉ #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
#align is_add_subgroup.add_mem_cancel_right
IsAddSubgroup.add_mem_cancel_right: โˆ€ {G : Type u_1} {a b : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s โ†’ a โˆˆ s โ†’ (b + a โˆˆ s โ†” b โˆˆ s)
IsAddSubgroup.add_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 โˆˆ s
h
:
a: G
a
โˆˆ
s: Set G
s
) :
a: G
a
*
b: G
b
โˆˆ
s: Set G
s
โ†”
b: G
b
โˆˆ
s: Set G
s
:= โŸจfun
hab: ?m.15379
hab
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.14510

A: Type ?u.14513

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s

h: a โˆˆ s

hab: a * b โˆˆ s



Goals accomplished! ๐Ÿ™
, hs.
mul_mem: โˆ€ {M : Type ?u.15398} [inst : Monoid M] {s : Set M}, IsSubmonoid s โ†’ โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
mul_mem
h: a โˆˆ s
h
โŸฉ #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
#align is_add_subgroup.add_mem_cancel_left
IsAddSubgroup.add_mem_cancel_left: โˆ€ {G : Type u_1} {a b : G} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s โ†’ a โˆˆ s โ†’ (a + b โˆˆ s โ†” b โˆˆ s)
IsAddSubgroup.add_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 โ†’ Prop
IsNormalAddSubgroup
[
AddGroup: Type ?u.16114 โ†’ Type ?u.16114
AddGroup
A: Type ?u.16101
A
] (
s: Set A
s
:
Set: Type ?u.16117 โ†’ Type ?u.16117
Set
A: Type ?u.16101
A
) extends
IsAddSubgroup: {A : Type ?u.16121} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsAddSubgroup
s: Set A
s
:
Prop: Type
Prop
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 โˆˆ s
normal
: โˆ€
n: ?m.16162
n
โˆˆ
s: Set A
s
, โˆ€
g: A
g
:
A: Type ?u.16101
A
,
g: A
g
+
n: ?m.16162
n
+ -
g: A
g
โˆˆ
s: Set A
s
#align is_normal_add_subgroup
IsNormalAddSubgroup: {A : Type u_1} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsNormalAddSubgroup
/-- `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. -/ @[
to_additive: {A : Type u_1} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
to_additive
] 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 s
IsNormalSubgroup
[
Group: Type ?u.17311 โ†’ Type ?u.17311
Group
G: Type ?u.17292
G
] (
s: Set G
s
:
Set: Type ?u.17314 โ†’ Type ?u.17314
Set
G: Type ?u.17292
G
) extends
IsSubgroup: {G : Type ?u.17318} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
:
Prop: Type
Prop
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โปยน โˆˆ s
normal
: โˆ€
n: ?m.17360
n
โˆˆ
s: Set G
s
, โˆ€
g: G
g
:
G: Type ?u.17292
G
,
g: G
g
*
n: ?m.17360
n
*
g: G
g
โปยน โˆˆ
s: Set G
s
#align is_normal_subgroup
IsNormalSubgroup: {G : Type u_1} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddCommGroup G] {s : Set G}, IsAddSubgroup s โ†’ IsNormalAddSubgroup s
to_additive
] theorem
isNormalSubgroup_of_commGroup: โˆ€ [inst : CommGroup G] {s : Set G}, IsSubgroup s โ†’ IsNormalSubgroup s
isNormalSubgroup_of_commGroup
[
CommGroup: Type ?u.18689 โ†’ Type ?u.18689
CommGroup
G: Type ?u.18670
G
] {
s: Set G
s
:
Set: Type ?u.18692 โ†’ Type ?u.18692
Set
G: Type ?u.18670
G
} (hs :
IsSubgroup: {G : Type ?u.18695} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
) :
IsNormalSubgroup: {G : Type ?u.18736} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
s: Set G
s
:= { hs with normal := fun
n: ?m.18820
n
hn: ?m.18823
hn
g: ?m.18826
g
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


1 * n โˆˆ s
G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


G: Type u_1

H: Type ?u.18673

A: Type ?u.18676

a, aโ‚, aโ‚‚, b, c: G

instโœ: CommGroup G

s: Set G

hs: IsSubgroup s

n: G

hn: n โˆˆ s

g: G


} #align is_normal_subgroup_of_comm_group
isNormalSubgroup_of_commGroup: โˆ€ {G : Type u_1} [inst : CommGroup G] {s : Set G}, IsSubgroup s โ†’ IsNormalSubgroup s
isNormalSubgroup_of_commGroup
#align is_normal_add_subgroup_of_add_comm_group
isNormalAddSubgroup_of_addCommGroup: โˆ€ {G : Type u_1} [inst : AddCommGroup G] {s : Set G}, IsAddSubgroup s โ†’ IsNormalAddSubgroup s
isNormalAddSubgroup_of_addCommGroup
theorem
Additive.isNormalAddSubgroup: โˆ€ [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ IsNormalAddSubgroup s
Additive.isNormalAddSubgroup
[
Group: Type ?u.19582 โ†’ Type ?u.19582
Group
G: Type ?u.19563
G
] {
s: Set G
s
:
Set: Type ?u.19585 โ†’ Type ?u.19585
Set
G: Type ?u.19563
G
} (hs :
IsNormalSubgroup: {G : Type ?u.19588} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
s: Set G
s
) : @
IsNormalAddSubgroup: {A : Type ?u.19619} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsNormalAddSubgroup
(
Additive: Type ?u.19620 โ†’ Type ?u.19620
Additive
G: Type ?u.19563
G
) _
s: Set G
s
:= @
IsNormalAddSubgroup.mk: โˆ€ {A : Type ?u.19638} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ (โˆ€ (n : A), n โˆˆ s โ†’ โˆ€ (g : A), g + n + -g โˆˆ s) โ†’ IsNormalAddSubgroup s
IsNormalAddSubgroup.mk
(
Additive: Type ?u.19639 โ†’ Type ?u.19639
Additive
G: Type ?u.19563
G
) _
_: Set (Additive G)
_
(
Additive.isAddSubgroup: โˆ€ {G : Type ?u.19659} [inst : Group G] {s : Set G}, IsSubgroup s โ†’ IsAddSubgroup s
Additive.isAddSubgroup
hs.
toIsSubgroup: โˆ€ {G : Type ?u.19690} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ IsSubgroup s
toIsSubgroup
) (@
IsNormalSubgroup.normal: โˆ€ {G : Type ?u.19704} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ โˆ€ (n : G), n โˆˆ s โ†’ โˆ€ (g : G), g * n * gโปยน โˆˆ s
IsNormalSubgroup.normal
_: Type ?u.19704
_
โ€นGroup (Additive G)โ€บ
_: Set ?m.19705
_
hs) -- porting note: Lean needs help synthesising #align additive.is_normal_add_subgroup
Additive.isNormalAddSubgroup: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ IsNormalAddSubgroup s
Additive.isNormalAddSubgroup
theorem
Additive.isNormalAddSubgroup_iff: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalAddSubgroup s โ†” IsNormalSubgroup s
Additive.isNormalAddSubgroup_iff
[
Group: Type ?u.20798 โ†’ Type ?u.20798
Group
G: Type ?u.20779
G
] {
s: Set G
s
:
Set: Type ?u.20801 โ†’ Type ?u.20801
Set
G: Type ?u.20779
G
} : @
IsNormalAddSubgroup: {A : Type ?u.20804} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsNormalAddSubgroup
(
Additive: Type ?u.20805 โ†’ Type ?u.20805
Additive
G: Type ?u.20779
G
) _
s: Set G
s
โ†”
IsNormalSubgroup: {G : Type ?u.20822} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
s: Set G
s
:= โŸจ

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.20782

A: Type ?u.20785

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G


G: Type u_1

H: Type ?u.20782

A: Type ?u.20785

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hโ‚: IsAddSubgroup s

hโ‚‚: โˆ€ (n : Additive G), n โˆˆ s โ†’ โˆ€ (g : Additive G), g + n + -g โˆˆ s


mk
G: Type u_1

H: Type ?u.20782

A: Type ?u.20785

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hโ‚: IsAddSubgroup s

hโ‚‚: โˆ€ (n : Additive G), n โˆˆ s โ†’ โˆ€ (g : Additive G), g + n + -g โˆˆ s


mk
G: Type u_1

H: Type ?u.20782

A: Type ?u.20785

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G



Goals accomplished! ๐Ÿ™
, fun
h: ?m.20842
h
=>
Additive.isNormalAddSubgroup: โˆ€ {G : Type ?u.20844} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ IsNormalAddSubgroup s
Additive.isNormalAddSubgroup
h: ?m.20842
h
โŸฉ #align additive.is_normal_add_subgroup_iff
Additive.isNormalAddSubgroup_iff: โˆ€ {G : Type u_1} [inst : Group G] {s : Set G}, IsNormalAddSubgroup s โ†” IsNormalSubgroup s
Additive.isNormalAddSubgroup_iff
theorem
Multiplicative.isNormalSubgroup: โˆ€ [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s โ†’ IsNormalSubgroup s
Multiplicative.isNormalSubgroup
[
AddGroup: Type ?u.21006 โ†’ Type ?u.21006
AddGroup
A: Type ?u.20993
A
] {
s: Set A
s
:
Set: Type ?u.21009 โ†’ Type ?u.21009
Set
A: Type ?u.20993
A
} (hs :
IsNormalAddSubgroup: {A : Type ?u.21012} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsNormalAddSubgroup
s: Set A
s
) : @
IsNormalSubgroup: {G : Type ?u.21042} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
(
Multiplicative: Type ?u.21043 โ†’ Type ?u.21043
Multiplicative
A: Type ?u.20993
A
) _
s: Set A
s
:= @
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 s
IsNormalSubgroup.mk
(
Multiplicative: Type ?u.21062 โ†’ Type ?u.21062
Multiplicative
A: Type ?u.20993
A
) _ _ (
Multiplicative.isSubgroup: โˆ€ {A : Type ?u.21082} [inst : AddGroup A] {s : Set A}, IsAddSubgroup s โ†’ IsSubgroup s
Multiplicative.isSubgroup
hs.
toIsAddSubgroup: โˆ€ {A : Type ?u.21111} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s โ†’ IsAddSubgroup s
toIsAddSubgroup
) (@
IsNormalAddSubgroup.normal: โˆ€ {A : Type ?u.21126} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s โ†’ โˆ€ (n : A), n โˆˆ s โ†’ โˆ€ (g : A), g + n + -g โˆˆ s
IsNormalAddSubgroup.normal
_: Type ?u.21126
_
โ€นAddGroup (Multiplicative A)โ€บ
_: Set ?m.21127
_
hs) #align multiplicative.is_normal_subgroup
Multiplicative.isNormalSubgroup: โˆ€ {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s โ†’ IsNormalSubgroup s
Multiplicative.isNormalSubgroup
theorem
Multiplicative.isNormalSubgroup_iff: โˆ€ [inst : AddGroup A] {s : Set A}, IsNormalSubgroup s โ†” IsNormalAddSubgroup s
Multiplicative.isNormalSubgroup_iff
[
AddGroup: Type ?u.22220 โ†’ Type ?u.22220
AddGroup
A: Type ?u.22207
A
] {
s: Set A
s
:
Set: Type ?u.22223 โ†’ Type ?u.22223
Set
A: Type ?u.22207
A
} : @
IsNormalSubgroup: {G : Type ?u.22226} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
(
Multiplicative: Type ?u.22227 โ†’ Type ?u.22227
Multiplicative
A: Type ?u.22207
A
) _
s: Set A
s
โ†”
IsNormalAddSubgroup: {A : Type ?u.22244} โ†’ [inst : AddGroup A] โ†’ Set A โ†’ Prop
IsNormalAddSubgroup
s: Set A
s
:= โŸจ

Goals accomplished! ๐Ÿ™
G: Type ?u.22201

H: Type ?u.22204

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœ: AddGroup A

s: Set A


G: Type ?u.22201

H: Type ?u.22204

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœ: AddGroup A

s: Set A

hโ‚: IsSubgroup s

hโ‚‚: โˆ€ (n : Multiplicative A), n โˆˆ s โ†’ โˆ€ (g : Multiplicative A), g * n * gโปยน โˆˆ s


mk
G: Type ?u.22201

H: Type ?u.22204

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœ: AddGroup A

s: Set A

hโ‚: IsSubgroup s

hโ‚‚: โˆ€ (n : Multiplicative A), n โˆˆ s โ†’ โˆ€ (g : Multiplicative A), g * n * gโปยน โˆˆ s


mk
G: Type ?u.22201

H: Type ?u.22204

A: Type u_1

a, aโ‚, aโ‚‚, b, c: G

instโœ: AddGroup A

s: Set A



Goals accomplished! ๐Ÿ™
, fun
h: ?m.22265
h
=>
Multiplicative.isNormalSubgroup: โˆ€ {A : Type ?u.22267} [inst : AddGroup A] {s : Set A}, IsNormalAddSubgroup s โ†’ IsNormalSubgroup s
Multiplicative.isNormalSubgroup
h: ?m.22265
h
โŸฉ #align multiplicative.is_normal_subgroup_iff
Multiplicative.isNormalSubgroup_iff: โˆ€ {A : Type u_1} [inst : AddGroup A] {s : Set A}, IsNormalSubgroup s โ†” IsNormalAddSubgroup s
Multiplicative.isNormalSubgroup_iff
namespace IsSubgroup variable [
Group: Type ?u.27820 โ†’ Type ?u.27820
Group
G: Type ?u.22407
G
] -- 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 โˆˆ s
to_additive
] theorem
mem_norm_comm: โˆ€ {s : Set G}, IsNormalSubgroup s โ†’ โˆ€ {a b : G}, a * b โˆˆ s โ†’ b * a โˆˆ s
mem_norm_comm
{
s: Set G
s
:
Set: Type ?u.22451 โ†’ Type ?u.22451
Set
G: Type ?u.22429
G
} (hs :
IsNormalSubgroup: {G : Type ?u.22454} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
s: Set G
s
) {
a: G
a
b: G
b
:
G: Type ?u.22429
G
} (
hab: a * b โˆˆ s
hab
:
a: G
a
*
b: G
b
โˆˆ
s: Set G
s
) :
b: G
b
*
a: G
a
โˆˆ
s: Set G
s
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s


b * a โˆˆ s
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s

h: aโปยน * (a * b) * aโปยนโปยน โˆˆ s


b * a โˆˆ s
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s


b * a โˆˆ s
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s

h: b * a โˆˆ s


b * a โˆˆ s
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s

h: b * a โˆˆ s


b * a โˆˆ s
G: Type u_1

H: Type ?u.22432

A: Type ?u.22435

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

hs: IsNormalSubgroup s

a, b: G

hab: a * b โˆˆ s


b * a โˆˆ s

Goals 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 โˆˆ s
IsSubgroup.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 โˆˆ s
IsAddSubgroup.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 โˆˆ s
to_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 โˆˆ s
mem_norm_comm_iff
{
s: Set G
s
:
Set: Type ?u.26125 โ†’ Type ?u.26125
Set
G: Type ?u.26103
G
} (hs :
IsNormalSubgroup: {G : Type ?u.26128} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
s: Set G
s
) {
a: G
a
b: G
b
:
G: Type ?u.26103
G
} :
a: G
a
*
b: G
b
โˆˆ
s: Set G
s
โ†”
b: G
b
*
a: G
a
โˆˆ
s: Set G
s
:= โŸจ
mem_norm_comm: โˆ€ {G : Type ?u.27295} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ โˆ€ {a b : G}, a * b โˆˆ s โ†’ b * a โˆˆ s
mem_norm_comm
hs,
mem_norm_comm: โˆ€ {G : Type ?u.27328} [inst : Group G] {s : Set G}, IsNormalSubgroup s โ†’ โˆ€ {a b : G}, a * b โˆˆ s โ†’ b * a โˆˆ s
mem_norm_comm
hsโŸฉ #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 โˆˆ s
IsSubgroup.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 โˆˆ s
IsAddSubgroup.mem_norm_comm_iff
/-- The trivial subgroup -/ @[
to_additive: (G : Type u_1) โ†’ [inst : AddGroup G] โ†’ Set G
to_additive
"the trivial additive subgroup"] def
trivial: (G : Type ?u.27395) โ†’ [inst : Group G] โ†’ Set G
trivial
(
G: Type ?u.27395
G
:
Type _: Type (?u.27395+1)
Type _
) [
Group: Type ?u.27398 โ†’ Type ?u.27398
Group
G: Type ?u.27395
G
] :
Set: Type ?u.27401 โ†’ Type ?u.27401
Set
G: Type ?u.27395
G
:= {
1: ?m.27423
1
} #align is_subgroup.trivial
IsSubgroup.trivial: (G : Type u_1) โ†’ [inst : Group G] โ†’ Set G
IsSubgroup.trivial
#align is_add_subgroup.trivial
IsAddSubgroup.trivial: (G : Type u_1) โ†’ [inst : AddGroup G] โ†’ Set G
IsAddSubgroup.trivial
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] {g : G}, g โˆˆ IsAddSubgroup.trivial G โ†” g = 0
to_additive
(attr := simp)] theorem
mem_trivial: โˆ€ {g : G}, g โˆˆ trivial G โ†” g = 1
mem_trivial
{
g: G
g
:
G: Type ?u.27801
G
} :
g: G
g
โˆˆ
trivial: (G : Type ?u.27830) โ†’ [inst : Group G] โ†’ Set G
trivial
G: Type ?u.27801
G
โ†”
g: G
g
=
1: ?m.27851
1
:=
mem_singleton_iff: โˆ€ {ฮฑ : Type ?u.28194} {a b : ฮฑ}, a โˆˆ {b} โ†” a = b
mem_singleton_iff
#align is_subgroup.mem_trivial
IsSubgroup.mem_trivial: โˆ€ {G : Type u_1} [inst : Group G] {g : G}, g โˆˆ trivial G โ†” g = 1
IsSubgroup.mem_trivial
#align is_add_subgroup.mem_trivial
IsAddSubgroup.mem_trivial: โˆ€ {G : Type u_1} [inst : AddGroup G] {g : G}, g โˆˆ IsAddSubgroup.trivial G โ†” g = 0
IsAddSubgroup.mem_trivial
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup (IsAddSubgroup.trivial G)
to_additive
] theorem
trivial_normal: IsNormalSubgroup (trivial G)
trivial_normal
:
IsNormalSubgroup: {G : Type ?u.28298} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
(
trivial: (G : Type ?u.28320) โ†’ [inst : Group G] โ†’ Set G
trivial
G: Type ?u.28276
G
) :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_1
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_2
โˆ€ {a b : G}, a โˆˆ trivial G โ†’ b โˆˆ trivial G โ†’ a * b โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_3
โˆ€ {a : G}, a โˆˆ trivial G โ†’ aโปยน โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_4
โˆ€ (n : G), n โˆˆ trivial G โ†’ โˆ€ (g : G), g * n * gโปยน โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_1
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_2
โˆ€ {a b : G}, a โˆˆ trivial G โ†’ b โˆˆ trivial G โ†’ a * b โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_3
โˆ€ {a : G}, a โˆˆ trivial G โ†’ aโปยน โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_4
โˆ€ (n : G), n โˆˆ trivial G โ†’ โˆ€ (g : G), g * n * gโปยน โˆˆ trivial G
G: Type u_1

H: Type ?u.28279

A: Type ?u.28282

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G



Goals accomplished! ๐Ÿ™
#align is_subgroup.trivial_normal
IsSubgroup.trivial_normal: โˆ€ {G : Type u_1} [inst : Group G], IsNormalSubgroup (trivial G)
IsSubgroup.trivial_normal
#align is_add_subgroup.trivial_normal
IsAddSubgroup.trivial_normal: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup (IsAddSubgroup.trivial G)
IsAddSubgroup.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 G
s
:
Set: Type ?u.34570 โ†’ Type ?u.34570
Set
G: Type ?u.34548
G
} (hs :
IsSubgroup: {G : Type ?u.34573} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
s: Set G
s
) :
s: Set G
s
=
trivial: (G : Type ?u.34606) โ†’ [inst : Group G] โ†’ Set G
trivial
G: Type ?u.34548
G
โ†” โˆ€
x: ?m.34611
x
โˆˆ
s: Set G
s
,
x: ?m.34611
x
= (
1: ?m.34652
1
:
G: Type ?u.34548
G
) :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.34551

A: Type ?u.34554

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s


s = trivial G โ†” โˆ€ (x : G), x โˆˆ s โ†’ x = 1
G: Type u_1

H: Type ?u.34551

A: Type ?u.34554

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s


(โˆ€ (x : G), x โˆˆ s โ†” x = 1) โ†” โˆ€ (x : G), x โˆˆ s โ†’ x = 1
G: Type u_1

H: Type ?u.34551

A: Type ?u.34554

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s


(โˆ€ (x : G), x โˆˆ s โ†” x = 1) โ†” โˆ€ (x : G), x โˆˆ s โ†’ x = 1
G: Type u_1

H: Type ?u.34551

A: Type ?u.34554

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

hs: IsSubgroup s


s = trivial G โ†” โˆ€ (x : G), x โˆˆ s โ†’ x = 1

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
#align is_add_subgroup.eq_trivial_iff
IsAddSubgroup.eq_trivial_iff: โˆ€ {G : Type u_1} [inst : AddGroup G] {s : Set G}, IsAddSubgroup s โ†’ (s = IsAddSubgroup.trivial G โ†” โˆ€ (x : G), x โˆˆ s โ†’ x = 0)
IsAddSubgroup.eq_trivial_iff
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup univ
to_additive
] theorem
univ_subgroup: IsNormalSubgroup univ
univ_subgroup
:
IsNormalSubgroup: {G : Type ?u.35615} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsNormalSubgroup
(@
univ: {ฮฑ : Type ?u.35637} โ†’ Set ฮฑ
univ
G: Type ?u.35593
G
) :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_1
1 โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_2
โˆ€ {a b : G}, a โˆˆ univ โ†’ b โˆˆ univ โ†’ a * b โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_3
โˆ€ {a : G}, a โˆˆ univ โ†’ aโปยน โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_4
โˆ€ (n : G), n โˆˆ univ โ†’ โˆ€ (g : G), g * n * gโปยน โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_1
1 โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_2
โˆ€ {a b : G}, a โˆˆ univ โ†’ b โˆˆ univ โ†’ a * b โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_3
โˆ€ {a : G}, a โˆˆ univ โ†’ aโปยน โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G


refine'_4
โˆ€ (n : G), n โˆˆ univ โ†’ โˆ€ (g : G), g * n * gโปยน โˆˆ univ
G: Type u_1

H: Type ?u.35596

A: Type ?u.35599

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G



Goals accomplished! ๐Ÿ™
#align is_subgroup.univ_subgroup
IsSubgroup.univ_subgroup: โˆ€ {G : Type u_1} [inst : Group G], IsNormalSubgroup univ
IsSubgroup.univ_subgroup
#align is_add_subgroup.univ_add_subgroup
IsAddSubgroup.univ_addSubgroup: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup univ
IsAddSubgroup.univ_addSubgroup
/-- The underlying set of the center of a group. -/ @[to_additive
addCenter: (G : Type u_1) โ†’ [inst : AddGroup G] โ†’ Set G
addCenter
"The underlying set of the center of an additive group."] def
center: (G : Type u_1) โ†’ [inst : Group G] โ†’ Set G
center
(
G: Type ?u.38576
G
:
Type _: Type (?u.38576+1)
Type _
) [
Group: Type ?u.38579 โ†’ Type ?u.38579
Group
G: Type ?u.38576
G
] :
Set: Type ?u.38582 โ†’ Type ?u.38582
Set
G: Type ?u.38576
G
:= {
z: ?m.38593
z
| โˆ€
g: ?m.38596
g
,
g: ?m.38596
g
*
z: ?m.38593
z
=
z: ?m.38593
z
*
g: ?m.38596
g
} #align is_subgroup.center
IsSubgroup.center: (G : Type u_1) โ†’ [inst : Group G] โ†’ Set G
IsSubgroup.center
#align is_add_subgroup.add_center
IsAddSubgroup.addCenter: (G : Type u_1) โ†’ [inst : AddGroup G] โ†’ Set G
IsAddSubgroup.addCenter
@[to_additive
mem_add_center: โˆ€ {G : Type u_1} [inst : AddGroup G] {a : G}, a โˆˆ IsAddSubgroup.addCenter G โ†” โˆ€ (g : G), g + a = a + g
mem_add_center
] theorem
mem_center: โˆ€ {a : G}, a โˆˆ center G โ†” โˆ€ (g : G), g * a = a * g
mem_center
{
a: G
a
:
G: Type ?u.39733
G
} :
a: G
a
โˆˆ
center: (G : Type ?u.39762) โ†’ [inst : Group G] โ†’ Set G
center
G: Type ?u.39733
G
โ†” โˆ€
g: ?m.39782
g
,
g: ?m.39782
g
*
a: G
a
=
a: G
a
*
g: ?m.39782
g
:=
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.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 * g
IsSubgroup.mem_center
#align is_add_subgroup.mem_add_center
IsAddSubgroup.mem_add_center: โˆ€ {G : Type u_1} [inst : AddGroup G] {a : G}, a โˆˆ IsAddSubgroup.addCenter G โ†” โˆ€ (g : G), g + a = a + g
IsAddSubgroup.mem_add_center
@[to_additive
add_center_normal: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup (IsAddSubgroup.addCenter G)
add_center_normal
] 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 โ†’ Prop
IsNormalSubgroup
(
center: (G : Type ?u.40952) โ†’ [inst : Group G] โ†’ Set G
center
G: Type ?u.40908
G
) := { one_mem :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G



Goals accomplished! ๐Ÿ™
mul_mem := fun
ha: ?m.41278
ha
hb: ?m.41281
hb
g: ?m.41284
g
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * aโœ * bโœ = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


aโœ * g * bโœ = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


aโœ * (g * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


aโœ * (bโœ * g) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


g * (aโœ * bโœ) = aโœ * bโœ * g
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

aโœ, bโœ: G

ha: aโœ โˆˆ center G

hb: bโœ โˆˆ center G

g: G


aโœ * bโœ * g = aโœ * bโœ * g

Goals accomplished! ๐Ÿ™
inv_mem := fun {
a: ?m.41304
a
}
ha: ?m.41307
ha
g: ?m.41310
g
=> calc
g: ?m.41310
g
*
a: ?m.41304
a
โปยน =
a: ?m.41304
a
โปยน * (
g: ?m.41310
g
*
a: ?m.41304
a
) *
a: ?m.41304
a
โปยน :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G



Goals accomplished! ๐Ÿ™
_: ?mโœ
_
=
a: ?m.41304
a
โปยน *
g: ?m.41310
g
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

a: G

ha: a โˆˆ center G

g: G



Goals accomplished! ๐Ÿ™
normal := fun
n: ?m.43573
n
ha: ?m.43576
ha
g: ?m.43579
g
h: ?m.43582
h
=> calc
h: ?m.43582
h
* (
g: ?m.43579
g
*
n: ?m.43573
n
*
g: ?m.43579
g
โปยน) =
h: ?m.43582
h
*
n: ?m.43573
n
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


h * (g * n * gโปยน) = h * n

Goals accomplished! ๐Ÿ™
_: ?mโœ
_
=
g: ?m.43579
g
*
g: ?m.43579
g
โปยน *
n: ?m.43573
n
*
h: ?m.43582
h
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


h * n = g * gโปยน * n * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


h * n = g * gโปยน * n * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


n * h = g * gโปยน * n * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


n * h = g * gโปยน * n * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


n * h = g * gโปยน * n * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


h * n = g * gโปยน * n * h

Goals accomplished! ๐Ÿ™
_: ?mโœ
_
=
g: ?m.43579
g
*
n: ?m.43573
n
*
g: ?m.43579
g
โปยน *
h: ?m.43582
h
:=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


g * (gโปยน * n) * h = g * n * gโปยน * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


g * (n * gโปยน) * h = g * n * gโปยน * h
G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G


G: Type u_1

H: Type ?u.40911

A: Type ?u.40914

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

n: G

ha: n โˆˆ center G

g, h: G



Goals accomplished! ๐Ÿ™
} #align is_subgroup.center_normal
IsSubgroup.center_normal: โˆ€ {G : Type u_1} [inst : Group G], IsNormalSubgroup (center G)
IsSubgroup.center_normal
#align is_add_subgroup.add_center_normal
IsAddSubgroup.add_center_normal: โˆ€ {G : Type u_1} [inst : AddGroup G], IsNormalAddSubgroup (IsAddSubgroup.addCenter G)
IsAddSubgroup.add_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`. -/ @[to_additive
addNormalizer: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ Set G โ†’ Set G
addNormalizer
"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 G
normalizer
(
s: Set G
s
:
Set: Type ?u.51199 โ†’ Type ?u.51199
Set
G: Type ?u.51177
G
) :
Set: Type ?u.51202 โ†’ Type ?u.51202
Set
G: Type ?u.51177
G
:= {
g: G
g
:
G: Type ?u.51177
G
| โˆ€
n: ?m.51213
n
,
n: ?m.51213
n
โˆˆ
s: Set G
s
โ†”
g: G
g
*
n: ?m.51213
n
*
g: G
g
โปยน โˆˆ
s: Set G
s
} #align is_subgroup.normalizer
IsSubgroup.normalizer: {G : Type u_1} โ†’ [inst : Group G] โ†’ Set G โ†’ Set G
IsSubgroup.normalizer
#align is_add_subgroup.add_normalizer
IsAddSubgroup.addNormalizer: {G : Type u_1} โ†’ [inst : AddGroup G] โ†’ Set G โ†’ Set G
IsAddSubgroup.addNormalizer
@[
to_additive: โˆ€ {G : Type u_1} [inst : AddGroup G] (s : Set G), IsAddSubgroup (IsAddSubgroup.addNormalizer s)
to_additive
] theorem
normalizer_isSubgroup: โˆ€ {G : Type u_1} [inst : Group G] (s : Set G), IsSubgroup (normalizer s)
normalizer_isSubgroup
(
s: Set G
s
:
Set: Type ?u.52526 โ†’ Type ?u.52526
Set
G: Type ?u.52504
G
) :
IsSubgroup: {G : Type ?u.52529} โ†’ [inst : Group G] โ†’ Set G โ†’ Prop
IsSubgroup
(
normalizer: {G : Type ?u.52551} โ†’ [inst : Group G] โ†’ Set G โ†’ Set G
normalizer
s: Set G
s
) := { one_mem :=

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

a, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G



Goals accomplished! ๐Ÿ™
mul_mem := fun {
a: ?m.52891
a
b: ?m.52894
b
} (
ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s
ha
: โˆ€
n: ?m.52898
n
,
n: ?m.52898
n
โˆˆ
s: Set G
s
โ†”
a: ?m.52891
a
*
n: ?m.52898
n
*
a: ?m.52891
a
โปยน โˆˆ
s: Set G
s
) (
hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s
hb
: โˆ€
n: ?m.54083
n
,
n: ?m.54083
n
โˆˆ
s: Set G
s
โ†”
b: ?m.52894
b
*
n: ?m.54083
n
*
b: ?m.52894
b
โปยน โˆˆ
s: Set G
s
)
n: ?m.54791
n
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, bโœ, c: G

instโœ: Group G

s: Set G

a, b: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

hb: โˆ€ (n : G), n โˆˆ s โ†” b * n * bโปยน โˆˆ s

n: G



Goals accomplished! ๐Ÿ™
inv_mem := fun {
a: ?m.54805
a
} (
ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s
ha
: โˆ€
n: ?m.54809
n
,
n: ?m.54809
n
โˆˆ
s: Set G
s
โ†”
a: ?m.54805
a
*
n: ?m.54809
n
*
a: ?m.54805
a
โปยน โˆˆ
s: Set G
s
)
n: ?m.55517
n
=>

Goals accomplished! ๐Ÿ™
G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G


G: Type u_1

H: Type ?u.52507

A: Type ?u.52510

aโœ, aโ‚, aโ‚‚, b, c: G

instโœ: Group G

s: Set G

a: G

ha: โˆ€ (n : G), n โˆˆ s โ†” a * n * aโปยน โˆˆ s

n: G



Goals accomplished! ๐Ÿ™
} #align is_subgroup.normalizer_is_subgroup
IsSubgroup.normalizer_isSubgroup: โˆ€ {G :