@[class]
- to_is_subring : is_subring S
- inv_mem : ∀ {x : F}, x ∈ S → x⁻¹ ∈ S
@[instance]
Equations
- is_subfield.field S = {add := comm_ring.add (show comm_ring ↥S, from subset.comm_ring), add_assoc := _, zero := comm_ring.zero (show comm_ring ↥S, from subset.comm_ring), zero_add := _, add_zero := _, neg := comm_ring.neg (show comm_ring ↥S, from subset.comm_ring), add_left_neg := _, add_comm := _, mul := comm_ring.mul (show comm_ring ↥S, from subset.comm_ring), mul_assoc := _, one := comm_ring.one (show comm_ring ↥S, from subset.comm_ring), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (x : ↥S), ⟨(↑x)⁻¹, _⟩, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
theorem
is_subfield.pow_mem
{F : Type u_1}
[field F]
{a : F}
{n : ℤ}
{s : set F}
[is_subfield s]
(h : a ∈ s) :
@[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] :
is_subfield (⇑f ⁻¹' 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] :
is_subfield (⇑f '' s)
@[instance]
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}
@[instance]
@[instance]
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}
[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)
[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)
[∀ (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)] :
is_subfield (set.Inter S)