Unbundled subfields (deprecated)

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 FieldTheory.Subfield, for subfields of fields.

Main definitions

IsSubfield (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

IsSubfield, subfield

structure IsSubfield {F : Type u_1} [Field F] (S : Set F) extends IsSubring S : Prop

IsSubfield (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.

• zero_mem : 0 ∈ S
• add_mem {a b : F} : a ∈ S → b ∈ S → a + b ∈ S
• neg_mem {a : F} : a ∈ S → -a ∈ S
• one_mem : 1 ∈ S
• mul_mem {a b : F} : a ∈ S → b ∈ S → a * b ∈ S
• inv_mem {x : F} : x ∈ S → x⁻¹ ∈ S

theorem IsSubfield.div_mem {F : Type u_1} [Field F] {S : Set F} (hS : IsSubfield S) {x y : F} (hx : x ∈ S) (hy : y ∈ S) : x / y ∈ S

theorem IsSubfield.pow_mem {F : Type u_1} [Field F] {a : F} {n : ℤ} {s : Set F} (hs : IsSubfield s) (h : a ∈ s) : a ^ n ∈ s

theorem Univ.isSubfield {F : Type u_1} [Field F] : IsSubfield Set.univ

theorem Preimage.isSubfield {F : Type u_1} [Field F] {K : Type u_2} [Field K] (f : F →+* K) {s : Set K} (hs : IsSubfield s) : IsSubfield (⇑f ⁻¹' s)

theorem Image.isSubfield {F : Type u_1} [Field F] {K : Type u_2} [Field K] (f : F →+* K) {s : Set F} (hs : IsSubfield s) : IsSubfield (⇑f '' s)

theorem Range.isSubfield {F : Type u_1} [Field F] {K : Type u_2} [Field K] (f : F →+* K) : IsSubfield (Set.range ⇑f)

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

• Field.closure S = {x : F | ∃ y ∈ Ring.closure S, ∃ 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.isSubmonoid {F : Type u_1} [Field F] {S : Set F} : IsSubmonoid (Field.closure S)

theorem Field.closure.isSubfield {F : Type u_1} [Field F] {S : Set F} : IsSubfield (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 : IsSubfield T) (H : S ⊆ T) : Field.closure S ⊆ T

theorem Field.closure_subset_iff {F : Type u_1} [Field F] {s t : Set F} (ht : IsSubfield 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 isSubfield_iUnion_of_directed {F : Type u_1} [Field F] {ι : Type u_2} [Nonempty ι] {s : ι → Set F} (hs : ∀ (i : ι), IsSubfield (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) : IsSubfield (⋃ (i : ι), s i)

theorem IsSubfield.inter {F : Type u_1} [Field F] {S₁ S₂ : Set F} (hS₁ : IsSubfield S₁) (hS₂ : IsSubfield S₂) : IsSubfield (S₁ ∩ S₂)

theorem IsSubfield.iInter {F : Type u_1} [Field F] {ι : Sort u_2} {S : ι → Set F} (h : ∀ (y : ι), IsSubfield (S y)) : IsSubfield (Set.iInter S)