∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Group G] [Finite G] [IsDomain k],
  Function.Injective ⇑(TannakaDuality.FiniteGroup.equivHom k G) ∧
    Function.Surjective ⇑(TannakaDuality.FiniteGroup.equivHom k G)