IsPrime typeclass?

Stream: mathlib4

[Kenny Lau]

image.png

https://loogle.lean-lang.org/?q=Ideal.IsPrime

Why does IsPrime sometimes show up as () (explicit argument) and sometimes as [] (auto typeclass)?

[Damiano Testa]

On superficial inspection, it seems to reflect whether the argument is explicit, even if it is a class.

[Andrew Yang]

Because they are sometimes declared as type class arguments and sometimes as explicit arguments

[Jovan Gerbscheid]

I guess which one is more convenient depends on the specific use case. They can both be used with dot-notation.