- to_is_subring : is_subring S
- inv_mem : ∀ {x : F}, x ∈ S → x⁻¹ ∈ S
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) :
theorem
is_subfield.pow_mem
{F : Type u_1}
[field F]
{a : F}
{n : ℤ}
{s : set F}
(hs : is_subfield s)
(h : a ∈ s) :
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) :
is_subfield (⇑f ⁻¹' 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) :
is_subfield (⇑f '' s)
field.closure s is the minimal subfield that includes s.
Equations
- field.closure S = {x : F | ∃ (y : F) (H : y ∈ ring.closure S) (z : F) (H : z ∈ ring.closure S), y / z = x}
theorem
field.mem_closure
{F : Type u_1}
[field F]
{S : set F}
{a : F}
(ha : a ∈ S) :
a ∈ field.closure S
theorem
field.closure_subset
{F : Type u_1}
[field F]
{S T : set F}
(hT : is_subfield T)
(H : S ⊆ T) :
field.closure S ⊆ T
theorem
field.closure_subset_iff
{F : Type u_1}
[field F]
{s t : set F}
(ht : is_subfield t) :
field.closure s ⊆ t ↔ 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)) :
is_subfield (set.Inter S)