title: Definition of multiplicative group of a field in Isabelle
body: <pre><code>theory Scratch
    imports
      &quot;HOL.Fields&quot;
      &quot;HOL.Groups&quot;
  begin
  
  locale Field_is_group=
    fixes F :: &quot;'a :: field&quot;
  begin
  typedef 'a mul_group = &quot;{x :: 'a set. x ≠ 0}&quot;
  end
  
  end
  </code></pre>
  <p>I'm new to Isabelle, and I have learned something about proving in first-order logic but not about data structures. I tried to formalize the proof of the fact that a field has a multiplicative group, but I don't know how to define the multiplicative group. It is the set of the whole field except zero, and a field in Isabelle is defined as a type. By looking about the references, I know I need use <code>typedef</code>, but it fails:</p>
  <pre><code>Type unification failed: No type arity set :: zero
  
  Failed to meet type constraint:
  
  Term:  λx. x ≠ 0 :: ??'b ⇒ bool
  Type:  'a set ⇒ ??'a
  
  The error(s) above occurred in typedef &quot;mul_group&quot;
  </code></pre>