Name of typeclass for algebraically closed fields

Stream: new members

[Isak Colboubrani]

Just out of curiosity: why is the typeclass for algebraically closed fields called IsAlgClosed instead of something like AlgebraicallyClosedField or a similar name?

Mathlib/FieldTheory/IsAlgClosed/Basic.lean-/-- Typeclass for algebraically closed fields. … --/
Mathlib/FieldTheory/IsAlgClosed/Basic.lean:class IsAlgClosed : Prop where …

[Ruben Van de Velde]

Prop-values typeclasses are generally named IsFoo to flag that fact

[Isak Colboubrani]

@Ruben Van de Velde Thanks! I see the point of the presence of the Is prefix, but what about a Field suffix? Would it be a bad idea to call it IsAlgClosedField to make it more grep:able and also in line with the naming say class IsPrincipalIdealRing (R : Type u) [Semiring R] : Prop …?

[Ruben Van de Velde]

I guess it could be, but it would be longer without being clearer, while you couldn't rename IsPrincipalIdealRing to IsPrincipalIdeal

[Isak Colboubrani]

I see the point. Thanks for clarifying!