Documentation

Mathlib.Algebra.Group.Subgroup.Even

Squares and even elements #

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

source
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
    Instances For
      source
      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
        Instances For
          source
          @[simp]
          theorem Subsemigroup.mem_square {S : Type u_1} [CommSemigroup S] {a : S} :
          a ∈ square S ↔ IsSquare a
          source
          @[simp]
          theorem AddSubsemigroup.mem_even {S : Type u_1} [AddCommSemigroup S] {a : S} :
          a ∈ even S ↔ Even a
          source
          @[simp]
          theorem Subsemigroup.coe_square {S : Type u_1} [CommSemigroup S] :
          ↑(square S) = {s : S | IsSquare s}
          source
          @[simp]
          theorem AddSubsemigroup.coe_even {S : Type u_1} [AddCommSemigroup S] :
          ↑(even S) = {s : S | Even s}
          source
          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
            Instances For
              source
              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
                Instances For
                  source
                  @[simp]
                  theorem Submonoid.square_toSubsemigroup {M : Type u_1} [CommMonoid M] :
                  (square M).toSubsemigroup = Subsemigroup.square M
                  source
                  @[simp]
                  theorem AddSubmonoid.even_toSubsemigroup {M : Type u_1} [AddCommMonoid M] :
                  (even M).toAddSubsemigroup = AddSubsemigroup.even M
                  source
                  @[simp]
                  theorem Submonoid.mem_square {M : Type u_1} [CommMonoid M] {a : M} :
                  a ∈ square M ↔ IsSquare a
                  source
                  @[simp]
                  theorem AddSubmonoid.mem_even {M : Type u_1} [AddCommMonoid M] {a : M} :
                  a ∈ even M ↔ Even a
                  source
                  @[simp]
                  theorem Submonoid.coe_square {M : Type u_1} [CommMonoid M] :
                  ↑(square M) = {s : M | IsSquare s}
                  source
                  @[simp]
                  theorem AddSubmonoid.coe_even {M : Type u_1} [AddCommMonoid M] :
                  ↑(even M) = {s : M | Even s}
                  source
                  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
                    Instances For
                      source
                      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
                        Instances For
                          source
                          @[simp]
                          theorem Subgroup.square_toSubmonoid {G : Type u_1} [CommGroup G] :
                          (square G).toSubmonoid = Submonoid.square G
                          source
                          @[simp]
                          theorem AddSubgroup.even_toAddSubmonoid {G : Type u_1} [AddCommGroup G] :
                          (even G).toAddSubmonoid = AddSubmonoid.even G
                          source
                          @[simp]
                          theorem Subgroup.mem_square {G : Type u_1} [CommGroup G] {a : G} :
                          a ∈ square G ↔ IsSquare a
                          source
                          @[simp]
                          theorem AddSubgroup.mem_even {G : Type u_1} [AddCommGroup G] {a : G} :
                          a ∈ even G ↔ Even a
                          source
                          @[simp]
                          theorem Subgroup.coe_square {G : Type u_1} [CommGroup G] :
                          ↑(square G) = {s : G | IsSquare s}
                          source
                          @[simp]
                          theorem AddSubgroup.coe_even {G : Type u_1} [AddCommGroup G] :
                          ↑(even G) = {s : G | Even s}