Documentation

Mathlib.GroupTheory.SpecificGroups.KleinFour

Klein Four Group #

The Klein (Vierergruppe) four-group is a non-cyclic abelian group with four elements, in which each element is self-inverse and in which composing any two of the three non-identity elements produces the third one.

Main definitions #

References #

TODO #

Tags #

non-cyclic abelian group

Klein four-groups as a mixin class #

class IsAddKleinFour (G : Type u_1) [AddGroup G] :

An (additive) Klein four-group is an (additive) group of cardinality four and exponent two.

Instances
    @[simp]
    theorem IsAddKleinFour.card_four {G : Type u_1} [AddGroup G] [self : IsAddKleinFour G] :
    class IsKleinFour (G : Type u_1) [Group G] :

    A Klein four-group is a group of cardinality four and exponent two.

    Instances
      @[simp]
      theorem IsKleinFour.card_four {G : Type u_1} [Group G] [self : IsKleinFour G] :
      @[simp]
      theorem IsKleinFour.exponent_two {G : Type u_1} [Group G] [self : IsKleinFour G] :
      Equations
      • =
      instance IsKleinFour.instFinite {G : Type u_1} [Group G] [IsKleinFour G] :
      Equations
      • =
      @[simp]
      theorem IsAddKleinFour.neg_eq_self {G : Type u_1} [AddGroup G] [IsAddKleinFour G] (x : G) :
      -x = x
      theorem IsKleinFour.inv_eq_self {G : Type u_1} [Group G] [IsKleinFour G] (x : G) :
      x⁻¹ = x
      theorem IsAddKleinFour.add_self {G : Type u_1} [AddGroup G] [IsAddKleinFour G] (x : G) :
      x + x = 0
      theorem IsKleinFour.mul_self {G : Type u_1} [Group G] [IsKleinFour G] (x : G) :
      x * x = 1
      theorem IsAddKleinFour.eq_finset_univ {G : Type u_1} [AddGroup G] [IsAddKleinFour G] [Fintype G] [DecidableEq G] {x : G} {y : G} (hx : x 0) (hy : y 0) (hxy : x y) :
      {x + y, x, y, 0} = Finset.univ
      theorem IsKleinFour.eq_finset_univ {G : Type u_1} [Group G] [IsKleinFour G] [Fintype G] [DecidableEq G] {x : G} {y : G} (hx : x 1) (hy : y 1) (hxy : x y) :
      {x * y, x, y, 1} = Finset.univ
      theorem IsAddKleinFour.eq_add_of_ne_all {G : Type u_1} [AddGroup G] [IsAddKleinFour G] {x : G} {y : G} {z : G} (hx : x 0) (hy : y 0) (hxy : x y) (hz : z 0) (hzx : z x) (hzy : z y) :
      z = x + y
      theorem IsKleinFour.eq_mul_of_ne_all {G : Type u_1} [Group G] [IsKleinFour G] {x : G} {y : G} {z : G} (hx : x 1) (hy : y 1) (hxy : x y) (hz : z 1) (hzx : z x) (hzy : z y) :
      z = x * y
      theorem IsAddKleinFour.addEquiv'.proof_1 {G₁ : Type u_2} {G₂ : Type u_1} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] (e : G₁ G₂) (he : e 0 = 0) (h : AddMonoid.exponent G₂ = 2) (x : G₁) (y : G₁) :
      e.toFun (x + y) = e.toFun x + e.toFun y
      def IsAddKleinFour.addEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] (e : G₁ G₂) (he : e 0 = 0) (h : AddMonoid.exponent G₂ = 2) :
      G₁ ≃+ G₂

      An equivalence between an IsAddKleinFour group G₁ and a group G₂ of exponent two which sends 0 : G₁ to 0 : G₂ is in fact an isomorphism.

      Equations
      Instances For
        def IsKleinFour.mulEquiv' {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsKleinFour G₁] (e : G₁ G₂) (he : e 1 = 1) (h : Monoid.exponent G₂ = 2) :
        G₁ ≃* G₂

        An equivalence between an IsKleinFour group G₁ and a group G₂ of exponent two which sends 1 : G₁ to 1 : G₂ is in fact an isomorphism.

        Equations
        Instances For
          @[reducible]
          def IsAddKleinFour.addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] [IsAddKleinFour G₂] (e : G₁ G₂) (he : e 0 = 0) :
          G₁ ≃+ G₂

          Any two IsAddKleinFour groups are isomorphic via any equivalence which sends the identity of one group to the identity of the other.

          Equations
          Instances For
            @[reducible]
            def IsKleinFour.mulEquiv {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsKleinFour G₁] [IsKleinFour G₂] (e : G₁ G₂) (he : e 1 = 1) :
            G₁ ≃* G₂

            Any two IsKleinFour groups are isomorphic via any equivalence which sends the identity of one group to the identity of the other.

            Equations
            Instances For
              theorem IsAddKleinFour.nonempty_addEquiv {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] [IsAddKleinFour G₁] [IsAddKleinFour G₂] :
              Nonempty (G₁ ≃+ G₂)

              Any two IsAddKleinFour groups are isomorphic.

              theorem IsKleinFour.nonempty_mulEquiv {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsKleinFour G₁] [IsKleinFour G₂] :
              Nonempty (G₁ ≃* G₂)

              Any two IsKleinFour groups are isomorphic.