## Stream: general

### Topic: subfield

#### Kenny Lau (Feb 20 2019 at 17:03):

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 (Feb 20 2019 at 17:03):

Question: what to do?

#### Kenny Lau (Feb 20 2019 at 17:15):

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

#### Johan Commelin (Feb 20 2019 at 17:17):

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

#### Kenny Lau (Feb 20 2019 at 17:18):

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

#### Chris Hughes (Feb 20 2019 at 17:19):

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

Last updated: May 13 2021 at 06:15 UTC