Why is is_subfield not a Prop?

Stream: new members

[Abhimanyu Pallavi Sudhir]

I want to define

variables {L : Type}
def subfields : set (set L) := {K' : set L | is_subfield K'}

But I run into a problem because is_subfield is somehow a Type, not a Prop. Why is this/how is this possible, and how can I fix the problem?

[Chris Hughes]

By mistake. It should be changed.

[Abhimanyu Pallavi Sudhir]

Do you know how I can circumvent the problem?

[Mario Carneiro]

you can use nonempty (is_subfield K')

[Chris Hughes]

#588

[Kevin Buzzard]

You can now also just update mathlib :-)