mathlib3 documentation

deprecated.subfield

Unbundled subfields (deprecated) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled subfields. Instead of using this file, please use subfield, defined in field_theory.subfield, for subfields of fields.

Main definitions #

is_subfield (S : set F) : Prop : the predicate that S is the underlying set of a subfield of the field F. The bundled variant subfield F should be used in preference to this.

Tags #

is_subfield

structure is_subfield {F : Type u_1} [field F] (S : set F) :

Prop

to_is_subring : is_subring S
inv_mem : ∀ {x : F}, x ∈ S → x⁻¹ ∈ S

is_subfield (S : set F) is the predicate saying that a given subset of a field is the set underlying a subfield. This structure is deprecated; use the bundled variant subfield F to model subfields of a field.

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] :

is_subfield set.univ

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)

theorem range.is_subfield {F : Type u_1} [field F] {K : Type u_2} [field K] (f : F →+* K) :

is_subfield (set.range ⇑f)

def field.closure {F : Type u_1} [field F] (S : set F) :

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.ring_closure_subset {F : Type u_1} [field F] {S : set F} :

ring.closure S ⊆ field.closure S

theorem field.closure.is_submonoid {F : Type u_1} [field F] {S : set F} :

is_submonoid (field.closure S)

theorem field.closure.is_subfield {F : Type u_1} [field F] {S : set F} :

is_subfield (field.closure S)

theorem field.mem_closure {F : Type u_1} [field F] {S : set F} {a : F} (ha : a ∈ S) :

a ∈ field.closure S

theorem field.subset_closure {F : Type u_1} [field F] {S : set F} :

S ⊆ 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 field.closure_mono {F : Type u_1} [field F] {s t : set F} (H : s ⊆ t) :

field.closure s ⊆ field.closure 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)