mathlib documentation

deprecated.subfield

theorem is_subfield.div_mem {F : Type u_1} [field F] {S : set F} [is_subfield S] {x y : F} (hx : x S) (hy : y S) :
x / y S
@[instance]
def is_subfield.field {F : Type u_1} [field F] (S : set F) [is_subfield S] :
Equations
theorem is_subfield.pow_mem {F : Type u_1} [field F] {a : F} {n : } {s : set F} [is_subfield s] (h : a s) :
a ^ n s
@[instance]
def univ.is_subfield {F : Type u_1} [field F] :
@[instance]
def preimage.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) (s : set K) [is_subfield s] :
@[instance]
def image.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) (s : set F) [is_subfield s] :
@[instance]
def 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} :
@[instance]
def field.closure.is_submonoid {F : Type u_1} [field F] {S : set F} :
@[instance]
def 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} [is_subfield T] (H : S T) :
theorem field.closure_subset_iff {F : Type u_1} [field F] (s t : set F) [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) [∀ (i : ι), is_subfield (s i)] (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_subfield (⋃ (i : ι), s i)
@[instance]
def is_subfield.inter {F : Type u_1} [field F] (S₁ S₂ : set F) [is_subfield S₁] [is_subfield S₂] :
is_subfield (S₁ S₂)
@[instance]
def is_subfield.Inter {F : Type u_1} [field F] {ι : Sort u_2} (S : ι → set F) [h : ∀ (y : ι), is_subfield (S y)] :