multiplicative group of a field

Stream: general

[Meow]

How to define the multiplicative group of a field in Lean 3?

[Meow]

import algebra.field
noncomputable theory

variables {K : Type*}[field K]

def mulgroup (h : ∀ (a : K), a ≠ 0) : comm_group K :=
{
  mul := λ x, λ y, x * y,
  inv := λ x, x⁻¹,
  one := 1,
  mul_comm :=
}

[Anupam Nayak]

Maybe this? https://leanprover-community.github.io/mathlib_docs/algebra/group/units.html#units

[Anupam Nayak]

See def units.group

[Meow]

Thanks

[Yury G. Kudryashov]

You can define anything (e.g., false) if you assume that all elements of a field are nonzero!

[Meow]

Yury G. Kudryashov said:

You can define anything (e.g., false) if you assume that all elements of a field are nonzero!

Yes I made a fool mistake, that's a contradiction.

[Adam Topaz]

The field itself will have a docs#group_with_zero instance which I think would be good enough for most things. If you really want, use docs#units which will have a group instance. But you will need to deal with coercions if you want to go back to the field

[Meow]

import tactic
import algebra.field
import algebra.ring.basic

noncomputable theory

universe u
structure mulgroup (α : Type u) [field α] (h: (0:α) ≠ (1:α)):=
(val : α)
(neq_zero : val ≠ 0)

instance (α : Type u) [field α] (h: (0:α) ≠ (1:α)): group (mulgroup α h) :=
{
  one := ⟨1, h.symm⟩,
  inv := λ u, ⟨u.val⁻¹,
    by {simp [mulgroup.neq_zero u]} ⟩,
  mul := λ u₁ u₂, ⟨u₁.val * u₂.val,
    by {simp [mulgroup.neq_zero u₁, mulgroup.neq_zero u₂]}⟩,
  mul_assoc := by finish,
  one_mul := by {simp, sorry},
  mul_one := sorry,
  mul_left_inv := sorry
}

How to complete the proof at the first sorry?
The goal of one_mul after simp is

α: Type u
_inst_1: field α
h: 0 ≠ 1
⊢ ∀ (a : mulgroup α h), {val := a.val, neq_zero := _} = a

That's trivial, but I don't know how to succeed.

[Kevin Buzzard]

Try intro a, cases a, refl

[Kevin Buzzard]

h is unnecessary by the way, it's an axiom of a field

[Meow]

Thanks

[Kevin Buzzard]

You have made a new structure, mulgroup, rather than using mathlib's units, so to get it to work effectively you will have to make a little interface for it. I would recommend proving an extensionality lemma for it before you start the proof that it's a group, ie prove that two terms of type mulgroup k (don't call it alpha unless you're actually a computer scientist who thinks this is a better name for a field) are equal when their vals are.

[Kevin Buzzard]

This might be as simple as writing @[ext] before the word structure but I'm not at lean to check. Then you will be able to use the ext tactic instead of cases

[Patrick Massot]

I was about to write that. Put @[ext] right above the structure line

[Yury G. Kudryashov]

BTW, all fields in mathlib are assumed to be nontrivial.

[Yury G. Kudryashov]

So you can get (0 : α) ≠ (1 : α) from docs#zero_ne_one.