Squares and even elements

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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