Squares and even elements

This file defines the subgroup of squares / even elements in an abelian group.

def Subsemigroup.square (S : Type u_1) [CommSemigroup S] : Subsemigroup S

In a commutative semigroup S, Subsemigroup.square S is the subsemigroup of squares in S.

Equations

• Subsemigroup.square S = { carrier := {s : S | IsSquare s}, mul_mem' := ⋯ }

def AddSubsemigroup.even (S : Type u_1) [AddCommSemigroup S] : AddSubsemigroup S

In a commutative additive semigroup S, AddSubsemigroup.even S is the subsemigroup of even elements in S.

Equations

• AddSubsemigroup.even S = { carrier := {s : S | Even s}, add_mem' := ⋯ }

@[simp]

theorem Subsemigroup.mem_square {S : Type u_1} [CommSemigroup S] {a : S} : a ∈ square S ↔ IsSquare a

@[simp]

theorem AddSubsemigroup.mem_even {S : Type u_1} [AddCommSemigroup S] {a : S} : a ∈ even S ↔ Even a

@[simp]

theorem Subsemigroup.coe_square {S : Type u_1} [CommSemigroup S] : ↑(square S) = {s : S | IsSquare s}

@[simp]

theorem AddSubsemigroup.coe_even {S : Type u_1} [AddCommSemigroup S] : ↑(even S) = {s : S | Even s}

def Submonoid.square (M : Type u_1) [CommMonoid M] : Submonoid M

In a commutative monoid M, Submonoid.square M is the submonoid of squares in M.

Equations

• Submonoid.square M = { toSubsemigroup := Subsemigroup.square M, one_mem' := ⋯ }

def AddSubmonoid.even (M : Type u_1) [AddCommMonoid M] : AddSubmonoid M

In a commutative additive monoid M, AddSubmonoid.even M is the submonoid of even elements in M.

Equations

• AddSubmonoid.even M = { toAddSubsemigroup := AddSubsemigroup.even M, zero_mem' := ⋯ }

@[simp]

theorem Submonoid.square_toSubsemigroup {M : Type u_1} [CommMonoid M] : (square M).toSubsemigroup = Subsemigroup.square M

@[simp]

theorem AddSubmonoid.even_toSubsemigroup {M : Type u_1} [AddCommMonoid M] : (even M).toAddSubsemigroup = AddSubsemigroup.even M

@[simp]

theorem Submonoid.mem_square {M : Type u_1} [CommMonoid M] {a : M} : a ∈ square M ↔ IsSquare a

@[simp]

theorem AddSubmonoid.mem_even {M : Type u_1} [AddCommMonoid M] {a : M} : a ∈ even M ↔ Even a

@[simp]

theorem Submonoid.coe_square {M : Type u_1} [CommMonoid M] : ↑(square M) = {s : M | IsSquare s}

@[simp]

theorem AddSubmonoid.coe_even {M : Type u_1} [AddCommMonoid M] : ↑(even M) = {s : M | Even s}

def Subgroup.square (G : Type u_1) [CommGroup G] : Subgroup G

In an abelian group G, Subgroup.square G is the subgroup of squares in G.

Equations

• Subgroup.square G = { toSubmonoid := Submonoid.square G, inv_mem' := ⋯ }

def AddSubgroup.even (G : Type u_1) [AddCommGroup G] : AddSubgroup G

In an abelian additive group G, AddSubgroup.even G is the subgroup of even elements in G.

Equations

• AddSubgroup.even G = { toAddSubmonoid := AddSubmonoid.even G, neg_mem' := ⋯ }

@[simp]

theorem Subgroup.square_toSubmonoid {G : Type u_1} [CommGroup G] : (square G).toSubmonoid = Submonoid.square G

@[simp]

theorem AddSubgroup.even_toAddSubmonoid {G : Type u_1} [AddCommGroup G] : (even G).toAddSubmonoid = AddSubmonoid.even G

@[simp]

theorem Subgroup.mem_square {G : Type u_1} [CommGroup G] {a : G} : a ∈ square G ↔ IsSquare a

@[simp]

theorem AddSubgroup.mem_even {G : Type u_1} [AddCommGroup G] {a : G} : a ∈ even G ↔ Even a

@[simp]

theorem Subgroup.coe_square {G : Type u_1} [CommGroup G] : ↑(square G) = {s : G | IsSquare s}

@[simp]

theorem AddSubgroup.coe_even {G : Type u_1} [AddCommGroup G] : ↑(even G) = {s : G | Even s}