coe Subgroup (Units F)

Stream: lean4

[Bolton Bailey]

This code was produced from working Lean 3 code, but in Lean 4 theres an error

import Mathlib.Data.Polynomial.FieldDivision
import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Subgroup.Finite
import Mathlib.Data.Polynomial.Eval
import Mathlib.GroupTheory.OrderOfElement

open scoped Classical

variable {k : Type} [Field k] [Fintype k]

noncomputable def vanishingPoly (G : Subgroup (Units k)) : Polynomial k :=
  Polynomial.monomial (Fintype.card G) 1 - Polynomial.C 1

theorem vanish_poly_for_subgroup_elem (G : Subgroup (Units k)) (g : G) :
    (vanishingPoly G).eval (g) = 0 :=
  by sorry

The issue is that it's not coercing the g to k. Can I do this somehow without having to write .val.val?

[Ruben Van de Velde]

((g : k\^x) : k)?

[Bolton Bailey]

Well yes, but without that either. It was one character before, can I just import something to get it to recognize it can coerce this?

[Kevin Buzzard]

Coercions have totally changed in lean 4. Maybe you can add the appropriate coercion? I would tell you what this is but I don't understand the new system.