Defining a group using `class`

Stream: new members

[Moti Ben-Ari]

In MIL 6.2 a group is defined and I want to prove mul_right_inv but I get errors. Here is the m(non)we:

import Mathlib.Tactic
namespace grp

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  mul_left_inv : ∀ x : α, mul (inv x) x = one

variable {G : ℚ} [Group₂ G]

theorem mul_right_inv (a : G) : mul a (inv a) = one := by
  have h : mul (  inv (mul a (inv a))
                  (mul (mul a (inv a)) (mul a (inv a))) ) = one := by
      rw [mul_assoc, ← mul_assoc inv a a, mul_left_inv, one_mul, mul_left_inv]
  rw [← h, ← mul_assoc, mul_left_inv, one_mul]
  done

The proof is translated from 2.2

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := by
  have h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1 := by
    rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
  rw [← h, ← mul_assoc, mul_left_inv, one_mul]

What am I missing?

Also, how do I go from mul, inv, one to * ⁻¹ 1?

[Yury G. Kudryashov]

Please provide a #mwe

[Markus Schmaus]

variable {G : ℚ} [Group₂ G]

The first part states that G is a rational number, rather than the rational numbers. And this results in a type error since the argent of your class is required to have type Type* not Q.

[Moti Ben-Ari]

Markus Schmaus said:

variable {G : ℚ} [Group₂ G]

The first part states that G is a rational number, rather than the rational numbers. And this results in a type error since the argent of your class is required to have type Type* not Q.

I understand. Changing to variable {G : Type*} [Group₂ G] I now get function expected at mul term has type ?m.76 at mul (inv a).

Actually, I want to prove the theorem for any group, not just for Int or S_n or any other specific group.

[Ruben Van de Velde]

Can you show the full code again?

[Moti Ben-Ari]

Ruben Van de Velde said:

Can you show the full code again?

import Mathlib.Tactic
namespace grp

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  mul_left_inv : ∀ x : α, mul (inv x) x = one

variable {G : Type*} [Group₂ G]

theorem mul_right_inv (a : G) : mul a (inv a) = one := by
  have h : mul (  inv (mul a (inv a))
                  (mul (mul a (inv a)) (mul a (inv a))) ) = one := by
      rw [mul_assoc, ← mul_assoc inv a a, mul_left_inv, one_mul, mul_left_inv]
  rw [← h, ← mul_assoc, mul_left_inv, one_mul]
  done

[Ruben Van de Velde]

open Group₂ on the line before theorem and then you'll find your parentheses aren't quite right :)

[Kevin Buzzard]

Or call it theorem Group₂.mul_right_inv

[Kevin Buzzard]

If you want a harder problem, delete mul_one and then try to prove mul_right_inv :-)