mathlib documentation

deprecated.subfield

@[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] :
a sa ^ 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] :
set Fset 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} :
a Sa field.closure 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] :
S Tfield.closure 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} :

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)] :
(∀ (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)] :