structure C06S02.Group₁ (α : Type u_1) : Type u_1

• mul : α → α → α
• one : α
• inv : α → α
• mul_assoc : ∀ (x y z : α), self.mul (self.mul x y) z = self.mul x (self.mul y z)
• mul_one : ∀ (x : α), self.mul x self.one = x
• one_mul : ∀ (x : α), self.mul self.one x = x
• inv_mul_cancel : ∀ (x : α), self.mul (self.inv x) x = self.one

theorem C06S02.Group₁.mul_assoc {α : Type u_1} (self : C06S02.Group₁ α) (x : α) (y : α) (z : α) : self.mul (self.mul x y) z = self.mul x (self.mul y z)

theorem C06S02.Group₁.mul_one {α : Type u_1} (self : C06S02.Group₁ α) (x : α) : self.mul x self.one = x

theorem C06S02.Group₁.one_mul {α : Type u_1} (self : C06S02.Group₁ α) (x : α) : self.mul self.one x = x

theorem C06S02.Group₁.inv_mul_cancel {α : Type u_1} (self : C06S02.Group₁ α) (x : α) : self.mul (self.inv x) x = self.one

structure C06S02.Group₁Cat : Type (u_1 + 1)

• α : Type u_1
• str : C06S02.Group₁ self.α

def C06S02.permGroup {α : Type u_1} : C06S02.Group₁ (Equiv.Perm α)

Equations

• C06S02.permGroup = { mul := fun (f g : Equiv.Perm α) => Equiv.trans g f, one := Equiv.refl α, inv := Equiv.symm, mul_assoc := ⋯, mul_one := ⋯, one_mul := ⋯, inv_mul_cancel := ⋯ }

structure C06S02.AddGroup₁ (α : Type u_1) : Type u_1

• add : α → α → α

theorem C06S02.Point.ext {x : C06S02.Point} {y : C06S02.Point} (x : x✝.x = y✝.x) (y : x✝.y = y✝.y) (z : x✝.z = y✝.z) : x✝ = y✝

theorem C06S02.Point.ext_iff {x : C06S02.Point} {y : C06S02.Point} : x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z = y.z

structure C06S02.Point : Type

• x : ℝ
• y : ℝ
• z : ℝ

def C06S02.Point.add (a : C06S02.Point) (b : C06S02.Point) : C06S02.Point

Equations

• a.add b = { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z }

def C06S02.Point.neg (a : C06S02.Point) : C06S02.Point

Equations

• a.neg = sorryAx C06S02.Point

def C06S02.Point.zero : C06S02.Point

Equations

• C06S02.Point.zero = sorryAx C06S02.Point

def C06S02.Point.addGroupPoint : C06S02.AddGroup₁ C06S02.Point

Equations

• C06S02.Point.addGroupPoint = sorryAx (C06S02.AddGroup₁ C06S02.Point)

class C06S02.Group₂ (α : Type u_1) : Type u_1

• mul : α → α → α
• one : α
• inv : α → α
• mul_assoc : ∀ (x y z : α), C06S02.Group₂.mul (C06S02.Group₂.mul x y) z = C06S02.Group₂.mul x (C06S02.Group₂.mul y z)
• mul_one : ∀ (x : α), C06S02.Group₂.mul x C06S02.Group₂.one = x
• one_mul : ∀ (x : α), C06S02.Group₂.mul C06S02.Group₂.one x = x
• inv_mul_cancel : ∀ (x : α), C06S02.Group₂.mul (C06S02.Group₂.inv x) x = C06S02.Group₂.one

theorem C06S02.Group₂.mul_assoc {α : Type u_1} [self : C06S02.Group₂ α] (x : α) (y : α) (z : α) : C06S02.Group₂.mul (C06S02.Group₂.mul x y) z = C06S02.Group₂.mul x (C06S02.Group₂.mul y z)

theorem C06S02.Group₂.mul_one {α : Type u_1} [self : C06S02.Group₂ α] (x : α) : C06S02.Group₂.mul x C06S02.Group₂.one = x

theorem C06S02.Group₂.one_mul {α : Type u_1} [self : C06S02.Group₂ α] (x : α) : C06S02.Group₂.mul C06S02.Group₂.one x = x

theorem C06S02.Group₂.inv_mul_cancel {α : Type u_1} [self : C06S02.Group₂ α] (x : α) : C06S02.Group₂.mul (C06S02.Group₂.inv x) x = C06S02.Group₂.one

instance C06S02.instGroup₂Perm {α : Type u_1} : C06S02.Group₂ (Equiv.Perm α)

Equations

• C06S02.instGroup₂Perm = { mul := fun (f g : Equiv.Perm α) => Equiv.trans g f, one := Equiv.refl α, inv := Equiv.symm, mul_assoc := ⋯, mul_one := ⋯, one_mul := ⋯, inv_mul_cancel := ⋯ }

def C06S02.mySquare {α : Type u_1} [C06S02.Group₂ α] (x : α) : α

Equations

• C06S02.mySquare x = C06S02.Group₂.mul x x

instance C06S02.instInhabitedPoint : Inhabited C06S02.Point

Equations

• C06S02.instInhabitedPoint = { default := { x := 0, y := 0, z := 0 } }

instance C06S02.instAddPoint : Add C06S02.Point

Equations

• C06S02.instAddPoint = { add := C06S02.Point.add }

instance C06S02.hasMulGroup₂ {α : Type u_1} [C06S02.Group₂ α] : Mul α

Equations

• C06S02.hasMulGroup₂ = { mul := C06S02.Group₂.mul }

instance C06S02.hasOneGroup₂ {α : Type u_1} [C06S02.Group₂ α] : One α

Equations

• C06S02.hasOneGroup₂ = { one := C06S02.Group₂.one }

instance C06S02.hasInvGroup₂ {α : Type u_1} [C06S02.Group₂ α] : Inv α

Equations

• C06S02.hasInvGroup₂ = { inv := C06S02.Group₂.inv }

def C06S02.foo {α : Type u_1} (f : Equiv.Perm α) (g : Equiv.Perm α) : f * 1 * g⁻¹ = (Equiv.symm g).trans ((Equiv.refl α).trans f)

Equations

• ⋯ = ⋯

class C06S02.AddGroup₂ (α : Type u_1) : Type u_1

• add : α → α → α