subfield

Stream: general

[Kenny Lau]

So the current definition of subfield is:

class is_subfield extends is_subring s : Prop :=
(inv_mem : ∀ {x : F}, x ∈ s → x⁻¹ ∈ s)

which is clearly wrong, as this requires the inverse of 0 to be inside the set.
However, if one fixes it, then a subfield would no longer be a field, because one would not have a computable inverse:

instance subset.field [is_subfield s] : field s :=
by subtype_instance

[Kenny Lau]

Question: what to do?

[Kenny Lau]

I think the solution to this nonsense is to define a structure field' where 0⁻¹ = 0

[Johan Commelin]

Maybe something like \for a b, a * b = 1, a \in S \to b \in S

[Kenny Lau]

this won't solve the problem that a subfield won't be a field

[Chris Hughes]

It will be a field it just won't be a field