Documentation

AlgebraInLean.Chapter01.Sheet04

source
instance AlgebraInLean.instGroupInt :
AlgebraInLean.Group ℤ
Equations
source
instance AlgebraInLean.instAbelianGroupInt :
AlgebraInLean.AbelianGroup ℤ
Equations
source
inductive AlgebraInLean.C₃ :
Type

The rotational symmetries of a regular triangle.

Instances For
    source
    def AlgebraInLean.C₃.op :
    AlgebraInLean.C₃ → AlgebraInLean.C₃ → AlgebraInLean.C₃
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def AlgebraInLean.C₃.inv :
      AlgebraInLean.C₃ → AlgebraInLean.C₃
      Equations
      Instances For
        source
        instance AlgebraInLean.instGroupC₃ :
        AlgebraInLean.Group AlgebraInLean.C₃
        Equations