Invalid binder annotation

Stream: new members

[YurySerdyuk]

What is wrong with my Lean4 code using Field type:

variable {𝕜 : Type} {M : Type}
variable [DecidableEq 𝕜] [Field 𝕜]

invalid binder annotation, type is not a class instance
?m.32

for [Field 𝕜] attribute.

[Alex J. Best]

What are your imports, can you give us a #mwe? You'll need to import some of mathlib to talk about fields for sure

[Kyle Miller]

This error looks like the auto-implicits feature is kicking in, which makes it hard to see that you don't have Field imported. For a better experience, try putting set_option relaxedAutoImplicit false at the top of your file, after the imports.