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}