mathlib documentation

deprecated.subfield

structure is_subfield {F : Type u_1} [field F] (S : set F) :
Prop
theorem is_subfield.div_mem {F : Type u_1} [field F] {S : set F} (hS : is_subfield S) {x y : F} (hx : x S) (hy : y S) :
x / y S
theorem is_subfield.pow_mem {F : Type u_1} [field F] {a : F} {n : } {s : set F} (hs : is_subfield s) (h : a s) :
a ^ n s
theorem univ.is_subfield {F : Type u_1} [field F] :
theorem preimage.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) {s : set K} (hs : is_subfield s) :
theorem image.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) {s : set F} (hs : is_subfield s) :
theorem range.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) :
def field.closure {F : Type u_1} [field F] (S : set F) :
set F

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

Equations
theorem field.ring_closure_subset {F : Type u_1} [field F] {S : set F} :
theorem field.closure.is_submonoid {F : Type u_1} [field F] {S : set F} :
theorem field.closure.is_subfield {F : Type u_1} [field F] {S : set F} :
theorem field.mem_closure {F : Type u_1} [field F] {S : set F} {a : F} (ha : a S) :
theorem field.subset_closure {F : Type u_1} [field F] {S : set F} :
theorem field.closure_subset {F : Type u_1} [field F] {S T : set F} (hT : is_subfield T) (H : S T) :
theorem field.closure_subset_iff {F : Type u_1} [field F] {s t : set F} (ht : is_subfield t) :
theorem field.closure_mono {F : Type u_1} [field F] {s t : set F} (H : s t) :
theorem is_subfield_Union_of_directed {F : Type u_1} [field F] {ι : Type u_2} [hι : nonempty ι] {s : ι → set F} (hs : ∀ (i : ι), is_subfield (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_subfield (⋃ (i : ι), s i)
theorem is_subfield.inter {F : Type u_1} [field F] {S₁ S₂ : set F} (hS₁ : is_subfield S₁) (hS₂ : is_subfield S₂) :
is_subfield (S₁ S₂)
theorem is_subfield.Inter {F : Type u_1} [field F] {ι : Sort u_2} {S : ι → set F} (h : ∀ (y : ι), is_subfield (S y)) :