# Unbundled subfields (deprecated) #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled subfields. Instead of using this file, please use Subfield, defined in FieldTheory.Subfield, for subfields of fields.

## Main definitions #

IsSubfield (S : Set F) : Prop : the predicate that S is the underlying set of a subfield of the field F. The bundled variant Subfield F should be used in preference to this.

## Tags #

IsSubfield, subfield

structure IsSubfield {F : Type u_1} [] (S : Set F) extends :

IsSubfield (S : Set F) is the predicate saying that a given subset of a field is the set underlying a subfield. This structure is deprecated; use the bundled variant Subfield F to model subfields of a field.

• zero_mem : 0 S
• add_mem : ∀ {a b : F}, a Sb Sa + b S
• neg_mem : ∀ {a : F}, a S-a S
• one_mem : 1 S
• mul_mem : ∀ {a b : F}, a Sb Sa * b S
• inv_mem : ∀ {x : F}, x Sx⁻¹ S
Instances For
theorem IsSubfield.inv_mem {F : Type u_1} [] {S : Set F} (self : ) {x : F} :
x Sx⁻¹ S
theorem IsSubfield.div_mem {F : Type u_1} [] {S : Set F} (hS : ) {x : F} {y : F} (hx : x S) (hy : y S) :
x / y S
theorem IsSubfield.pow_mem {F : Type u_1} [] {a : F} {n : } {s : Set F} (hs : ) (h : a s) :
a ^ n s
theorem Univ.isSubfield {F : Type u_1} [] :
IsSubfield Set.univ
theorem Preimage.isSubfield {F : Type u_1} [] {K : Type u_2} [] (f : F →+* K) {s : Set K} (hs : ) :
theorem Image.isSubfield {F : Type u_1} [] {K : Type u_2} [] (f : F →+* K) {s : Set F} (hs : ) :
IsSubfield (f '' s)
theorem Range.isSubfield {F : Type u_1} [] {K : Type u_2} [] (f : F →+* K) :
def Field.closure {F : Type u_1} [] (S : Set F) :
Set F

Field.closure s is the minimal subfield that includes s.

Equations
• = {x : F | y ∈ , z ∈ , y / z = x}
Instances For
theorem Field.ring_closure_subset {F : Type u_1} [] {S : Set F} :
theorem Field.closure.isSubmonoid {F : Type u_1} [] {S : Set F} :
theorem Field.closure.isSubfield {F : Type u_1} [] {S : Set F} :
theorem Field.mem_closure {F : Type u_1} [] {S : Set F} {a : F} (ha : a S) :
theorem Field.subset_closure {F : Type u_1} [] {S : Set F} :
theorem Field.closure_subset {F : Type u_1} [] {S : Set F} {T : Set F} (hT : ) (H : S T) :
theorem Field.closure_subset_iff {F : Type u_1} [] {s : Set F} {t : Set F} (ht : ) :
s t
theorem Field.closure_mono {F : Type u_1} [] {s : Set F} {t : Set F} (H : s t) :
theorem isSubfield_iUnion_of_directed {F : Type u_1} [] {ι : Type u_2} [] {s : ιSet F} (hs : ∀ (i : ι), IsSubfield (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
IsSubfield (⋃ (i : ι), s i)
theorem IsSubfield.inter {F : Type u_1} [] {S₁ : Set F} {S₂ : Set F} (hS₁ : ) (hS₂ : ) :
IsSubfield (S₁ S₂)
theorem IsSubfield.iInter {F : Type u_1} [] {ι : Sort u_2} {S : ιSet F} (h : ∀ (y : ι), IsSubfield (S y)) :